The Safety-Critical Systems Lectures Series


Contributions by

Jan Peleska

Jan Bredereke

Stefan Bisanz

Aliki Tsiolakis


Context of this Lectures Series

This is a series of lectures and seminars of our initiative Graduate Studies in Safety-Critical Systems. It is intended for an international audience of engineers working in the field, graduate students working on their Diploma, Masters, PhD of Habilitation degrees in computer science or electrical engineering. Due to the international character of the initiative, lectures will be held in English. At present, the lecture series is divided into three parts, each part planned as a two hours/week lecture for one semester:


Objectives and summary of the Safety-Critical Systems III Lecture

The third part of the Safety-Critical Systems lecture series focuses on concrete problems arising in specific types of safety-critical systems, and methods and tools which are suitable for modelling, verification, validation and test (VVT) of these problems.

Both for the development and for VVT of safety-critical systems, it is mandatory to have a precise model describing the intended behaviour of the system on an abstract level, that is, without referring implementation details. In the world of safety-critical control systems, the control tasks often involve both discrete and time-continuous observables: The former have a finite domain and change at discrete points in time (switches, traffic lights, points ...) while the latter are (at least conceptually) piecewise continuous functions over time (temperature, pressure, thrust ...). As a consequence, the modelling formalisms must be capable of incorporating both the discrete and time-continuous aspects. To this end, we will use Henzinger's definition of Hybrid Automata as the most general modelling technique which can be used to capture all possible aspects in the context of safety-critical real-time systems we can think of. The theoretical notions of safety conditions and liveness conditions will be introduced and related to the practical notion of safety-related assertions.

For a concrete problem from the field of safety-critical systems it may be advisable to use less general models than Henzinger's Hybrid Automata:

At least on an intuitive level the specification formalisms listed above can be viewed as restrictions of the Henzinger's Hybrid Automata. (Of course, on a formal level, it may be quite hard to map a specification written in one formalism [such as Z] into a semantically equivalent representation in another one [such as Hybrid Automata].) The practical examples to be used for modelling safety-related aspects of control systems are chosen from the following list: To tackle the examples sketched above, we may use the following tools for modelling and analysis: The tools are freely available for this lecture. Most of them can be used with Linux.


Related Activities of Other Groups and Organisations


References

More references will be introduced during the lectures!


Software


Specifications used in the lectures


Exercises


Jan Peleska / TZI - Bremen Institute of Safe Systems BISS / < jp@informatik.uni-bremen.de> / 22-JAN-2002