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 and home assignment.

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

Tutorials: Wed 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 scientific articles.

Lecturer: Lic.Sc.(Tech.) Keijo Heljanko, email: Keijo.Heljanko@hut.fi, tel. 451 3256, office hours Mon 13-14 in room TB334.

Course assistant: M.A. Misa Keinänen, email: Misa.Keinanen@hut.fi, tel. 451 3364.