For the most recent entries see the Petri Nets Newsletter.

A Case Study in Design and Validation of Reactive Systems by Means of Petri Nets.

Heiner, Monika; Deussen, P.

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

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography