In: Proc. High Performance Computing `98, Boston, April 1998, pages 394-403. San Diego: SCS Int., 1998. ISBN 1-56555-145-1.
Abstract: The development of provably error-free concurrent systems is still a challenge of practical system engineering. Modeling 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. These alternative approaches are summarized and compared with each other: structural analysis, integer programming, compressed and composite state space representations, lazy state space constructions, and partial order representations. It is demonstrated by means of case studies 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 qualitative system properties (consistency, safety, progress) of the concurrent control software of reactive systems is exemplified. If possible, different analysis techniques are applied and compared with each other concerning their pros and cons. The main lesson learned is that the different methods do not compete, but complement each other. Finally, objectives of an open integrated tool box to support Petri net based dependability engineering are outlined.
Keywords: hierarchical place/transition nets; temporal logics; verification; static analysis; model checking; reactive systems.
Back to the Petri Nets Bibliography