In: Proc. IMACS Multiconference on Computational Engineering in Systems Applications (CESA `96), Symposium `Discrete Events and Manufacturing Systems', Lille, July 1996, pages 121-126. 1996. Available at http://www.informatik.tu-cottbus.de/~wwwdssz/publications/papers.html.
Abstract: The development of provably error-free concurrent systems is still a challenge of system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well-known approaches using formal methods. To evaluate the reached practicability degree of available methods and tools to at least medium-sized systems, we demonstrate the step-wise development and validation of the control software of a reactive system. The validation of qualitative properties comprises two steps. At first, context checking of general semantic properties is done by a suitable combination of static and dynamic analysis techniques of Petri net theory. Afterwards, verification of well-defined special semantic properties, especially safety properties, given by a separate specification of the required functionality, is performed by model checking. Strong emphasis has been laid on automation of the analyses to be done.
Keywords: Parallel software/system engineering; static analysis; formal methods; Petri nets; temporal logics; control software; reactive system; discrete event systems; reliability.