T-79.186 Reactive Systems (2 cr) P

Spring 2005

Previous years: [Spring 2004] [Spring 2003] [Spring 2002] [Spring 2001] [Spring 2000] [Spring 1999]

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 stimulus provided by the environment.

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

The 1997 "Nobel prize of computer science", the A. M. Turing award, was given to Amir Pnueli, a pioneer of verification of reactive systems:

"It is time that formal verification (of both software and hardware systems) be demoted from an art practiced by the enlightened few to an activity routinely and mundanely performed by a cadre of Verification Engineers (a new profession), as a standard part of the system development process."

The contents of the course include the modeling of reactive systems, specification of properties using temporal logic, and the verification of such properties. In addition, basics of model checking algorithms are introduced, and their underlying theory is explored.

Requirements: Seminar talks, home exercises, and project work.

Lectures: Mon 16.15-18 in room TB353 (CS-building), first lecture on Mon 24th of Jan.

Tutorials: Mon 18-18:45 in room TB353 (CS-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, O. Grumberg, and D.A. Peled: Model Checking, 314 p., MIT Press 1999, (Chapters 3, 9-13).

In addition lecture slides and scientific articles.

Lectures: D.Sc.(Tech.), Academy Research Fellow Keijo Heljanko.

Tutorials: M.A. Misa Keinänen.