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:
- Safety-Critical Systems I: Basic concepts - problems - methods - techniques
- Safety-Critical Systems II: Management aspects - standards - V-Models - TQM - assessment -
process improvement
- Safety-Critical Systems III: Formal methods and tools - model checking - testing -
partial verification - inspection techniques - case studies
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:
- If safety aspects may be properly expressed by invariants on
discrete observables and by conditions on sequential variable
transformations, the Z notation provides a practical means for
specification and formal analysis of these aspects.
- If safety aspects refer to the causal behaviour of a system
(sequencing and synchronisation of events), CSP is an appropriate
candidate for specification and VVT of these aspects.
- If observables are discrete, but timing constraints are relevant
to express safety conditions, Timed CSP and a number of Timed Automata
formalisms are the most suitable candidates for modelling and VVT.
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:
- The elevator specification: this is a must when introducing
safety-related systems. You better get over it in this lecture,
otherwise it will haunt you until the end of your days. This will be
modelled and analysed in Z.
- The Mirrored Disk algorithm: A simple example from the world of
fault-tolerant systems, may be adequately modelled using CSP. Further
examples can be selected on demand from the world of operating systems.
- Safe buffered Reader-Writer Communication in real-time: This is a
set of standard mechanisms used for data exchange between tasks in
real-time systems: To ensure that communication will take place without
buffer overflow and without illegal interference between readers and
writers, it is necessary to impose some timing restrictions upon the
communicating tasks. Here we need a formalism with time (timed
automata) for modelling and verification.
- Railway crossing problem: This involves hybrid modelling, since
braking a train to prevent it from running into an unsafe crossing is
best modelled by differentiable functions.
To tackle the examples sketched above, we may use the following tools
for modelling and analysis:
- Mike Spivey's Z type checker for the Z notation
- The FDR tool for model checking untimed CSP.
- The UPPAAL tool for model checking timed automata.
- The RT-Tester tool for automated test and simulation with Timed CSP.
- Henzinger's HYTEC tool for the analysis of Hybrid Automata.
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
- Specification for the session using the Z
notation:
The Elevator (elevator.fuzz source file),
The Elevator (elevator.ps postscript file)
- CSP specifications for elevator simulation with RT-Tester and
Stefan's Java-Simulation, including watchdog specification sample,
configuration file config.rtt and graphics configuration file
ele.graphics for rttview:
elevator_csp.tgz (unpack with tar xzvf elevator_csp.tgz).
Note: The DOOR specification contains a safety violation which
will be detected by watchdog.
- CSP specifications for the Mirrored Disk algorithm
(mirdd.csp)
Exercises
Jan Peleska
/ TZI - Bremen Institute of Safe Systems BISS /
<
jp@informatik.uni-bremen.de>
/ 22-JAN-2002