T-79.5301 Reactive Systems (4 cr) P

Spring 2007 (Periods III and IV)

Previous years: [Spring 2006]

Reactive systems can be found in many embedded systems such as microprocessors, telecommunication systems and data communication networks. Their central feature is non-terminating behavior and reaction to stimuli provided by the environment.

The modeling and verification of reactive systems has become a natural part of the system development cycle in the design of VLSI circuits. Similar techniques can also be applied, e.g., to the design and implementation of data communication protocols.

The course covers the basic theory of modeling reactive systems using automata, specifying requirements on the behavior of such models using temporal logic, and verifying these properties using model checking algorithms.

Seminars: Tuesdays 16-18 in room TB353 (Computer Science building).

Tutorials: Tuesdays 18-19 in room TB353 (Computer Science building).

Literature: B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, and P. McKenzie: Systems and Software Verification - Model-Checking Techniques and Tools, 190 p., Springer, 1999. [Chapters 1-2, 6-11]

E. M. Clarke Jr., O. Grumberg, and D. A. Peled: Model Checking, 314 p., The MIT Press, 1999. [Chapters 3-4, 9-10]

Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems - Specification, Springer, 1992. [Chapters 3.2-3.3, 4.2]

Course coordinator: Heikki Tauriainen.

To pass the course, you should:

1. give two seminar talks (30-40 min / talk)
2. earn at least 20 points (total) from four home assignments (10 points / assignment)

Schedule for Spring 2007

Final results of the course (11 May, 2007)