KIV

Abstract

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.