Formal Development of a Distributed Control System for Road Marking Machines

Peter Herrmann, Manfred Noël

Universität Dortmund, FB Informatik, LS IV, D-44221 Dortmund
E-Mail: Peter.Herrmann@cs.tu-dortmund.de, Manfred.Noel@t-online.de

Abstract

Formal specification and verification of large distributed systems, like computer controlled technical plants, is a rather demanding task. In spite of its complexity, a system should be described in a clear and easily understandable way. Moreover, one should be able to verify important system properties within an acceptable amount of time. The formal specification technique cTLA facilitates the development of complex system descriptions. A system specification is composed from much simpler behavior constraint descriptions each modeling only a certain part of a system component. The compositionality of cTLA and the modularity of the system specifications make proofs of system properties easier, too. Mostly, a system property is not fulfilled by the whole system but by the interaction of some system components. This is reflected in the cTLA proofs which are performed by partial, less complex subsystem models describing only relevant system parts.

In this article, we show the use of cTLA to specify and verify distributed hybrid technical systems by means of an application in practice. Due to a German state regulation, producers and users of road marking machines have to prove formally that the thickness of the applied road markings obey certain limits. The use of cTLA to specify a particular road marking machine as well as to perform the formal proof that this machine obeys the required limits are described.

Published in

Proceedings of the 8th International Conference on Telecommunication Systems - Modeling and Analysis, pages 430-437, ATSMA, IFIP, 2000.

Obtaining the paper

Due to the copyright agreement between the publisher and the authors we are not allowed to make the paper available online. If you have problems to obtain it, please call us.