Formal Models for Parallel and Distributed Systems

RISC-Linz logo

Wolfgang Schreiner
326.619 (SS 2001)
Wed 16:30-18:00, Hagenberg

Modeling of and Reasoning about Reactive Systems

A reactive system maintains an ongoing interaction with its environment, as opposed to computing some final value on termination. Examples of reactive systems are concurrent programs, embedded and process control programs, and operating systems.

Reactive systems have a complex nature; a merely intuitive understanding is not sufficient to draw conclusions about their behavior. For the specification and design of such system, a professional engineer therefore needs formal frameworks that allow to model the system and to reason about its behavior.

This course focuses on two such frameworks:

Temporal Logic
Temporal logic describes and reasons about sequences of states evolving in time. A reactive system is translated into a logic formula; an implementation meets a specification, if the implementation implies the specification.
Process Calculus
Process calculus describes and reasons about the interaction of a system with its environment. The system is translated into an expression that can be transformed according to a set of algebraic laws without changing its observational behavior.

The course will provide the necessary formal basis but then concentrate on the application of these frameworks for designing correct reactive systems.

Literature

Leslie Lamport
The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994.
Leslie Lamport
Specifying Concurrent Systems with TLA+, Calculational System Design. M. Broy and R. Steinbrüggen, editors, IOS Press, Amsterdam, 1999.
Leslie Lamport
TLA in Pictures, IEEE Transactions on Software Engineering 21, 9, (September 1995) 768-775.
Zohar Manna and Amir Pnueli
Temporal Verification of Reactive Systems -- Safety, Springer, New York, 1995.
Robin Milner
Communication and Concurrency, Prencice Hall, Englewood Cliffs, NJ, 1989.

Slides

The Temporal Logic of Actions I (PostScript)
Logic of actions, the raw logic, TLA, fairness, syntax and semantics of TLA, proof rules.
The Temporal Logic of Actions II (PostScript)
Proving simple program properties, invariance proofs, eventuality proofs, proof of fairness, formal specification, quantification, refinement mappings.
A Process Calculus I (PostScript)
Agents and behaviors, exxamples, composition of agents, equality of agents, restrictions, transition graphs, the basic language, derivation trees, the value-passing calculus.
A Process Calculus II (PostScript)
Equational laws, equivalence of agents, strong bisimulation and strong equivalence, weak bisimulation and observation equivalence, observation congruence.

Maintained by: Wolfgang Schreiner
Last Modification: June 29, 2001

[Up] [RISC-Linz] [University] [Search]