1995: Techn. Report No. I-08. BTU Cottbus, December 1995. 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 Petri net based step-wise development and validation of the control software of a reactive system. The validation of qualitative properties comprises two steps. At first, the context checking of general semantic properties is done by a suitable combination of static and dynamic analysis techniques, mainly of ``classical'' Petri net theory. Afterwards, the 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.
This case study has been already investigated by a lot of different formal methods. This paper provides the possibility to take into account also a strongly Petri net-oriented approach to compare advantages and drawbacks inherent to different formal methods.
Keywords: Parallel software/system engineering; validation; static analysis; formal methods; Petri nets; temporal logics; control software; production cell.