Hide menu

FDA130 Formal Modeling and Verification for Real-Time Systems (CIS)

Lectures:

32 hours.

Recommended for

Graduate students, researchers, practitioners.

The course was last given:

New course.

Goals

To provide theoretical basics and to introduce advanced research issues. Examples will be presented and some state of the art tools will be discussed.

Prerequisites

Basic knowledge in logics, modeling and real-time systems.

Organization

Lectures.

Contents

Introduction

Discrete and continuous time; modeling

Model checking basics

Temporal logics
Explicit state model checking
Symbolic model checking

Model checking for discrete real-time

RTCTL model checking
Quantitative analysis

Models for continuous real-time

Timed automata
Time Petri nets

Model checking for timed automata

Region graph
Zone automaton
Time-abstract (bi)simulations
Tools: UPPAAL, KRONOS

Advanced model checking issues:

Symbolic representation
Partial order reduction

Languages for real-time systems:

SDL
Synchronous languages

Real-time system design and analysis:

Compositionality issues
Scheduling and control
High-level design and refinement

Literature

Research papers.

Teacher

Marius Minea.

Examiner

Petru Eles, Zebo Peng.

Schedule

Fall 2002.

Examination

To be decided.

Credit

6 credits.


Page responsible: Anne Moe