Model Checking Safety Properties in Modular High-Level Nets

11 years 12 months ago
Model Checking Safety Properties in Modular High-Level Nets
Model checking by exhaustive state space enumeration is one of the most developed analysis methods for distributed event systems. Its main problem—the size of the state spaces—has been addressed by various reduction methods. Complex systems tend to consist of loosely connected modules, which may perform internal tasks in parallel. The possible interleavings of these parallel tasks easily leads to a large number of reachable global states. In modular state space analysis, the internal actions are explored separately in each module, and the global state space only includes synchronisations. This article introduces nested modular nets, which are hierarchal collections of nets synchronising via shared transitions, and presents a simple algorithm for model checking safety properties in modular systems.
Marko Mäkelä
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where APN
Authors Marko Mäkelä
Comments (0)