ON EXPLOITING THE ANALYSIS POWER OF PETRI NETS FOR THE VALIDATION OF DISCRETE EVENT SYSTEMS
Monika Heiner · 1997
Abstract: The development of provably error-free concurrent systems is still a challenge of practical system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well-known approaches using formal methods. Among those Petri net analysis techniques suitable for strong verification purposes there is an increasing amount of promising methods avoiding the construction of the complete interleaving state space, and by this way the well-known state explosion problem. This paper claims to demonstrate that the available methods and tools are actually applicable successfully to at least medium-sized systems. For that purpose, the step-wise validation of various system properties (consistency, safety, progress) of the concurrent control software of a reactive system is performed. If possible, different analysis techniques are applied and compared with each other concerning its efforts.