Formal Models for Parallel and Distributed Systems

Wolfgang Schreiner
326.619, Mon 8:30-10:00, T711
WS 1999/2000 (Start: October 11)

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.

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.