Specification and verification of distributed technical systems with central control

This paper presents an algebraic approach to the specification
and verification of distributed technical systems, which are
controlled by a central control program. The approach is
demonstrated by its application to the case study "production
cell". The approach uses first-order specifications to describe
the possible behaviour of the system. Specifications are
structured according to the physical structure of the system. A
PASCAL-like program is used to enforce intended behaviour.
The whole case study, including specification as well as
verification of lifeness and safety conditions, is carried out
using the KIV system.

This research was sponsored by the BMFT project KORSO.