## Formal Models for Parallel and Distributed Systems |

**
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.

**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.

**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]