Title :
A new compositional method for condensed state-space verification
Author :
Juan, Eric Y T ; Tsai, Jeffrey J P ; Murata, Tadao
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Illinois Univ., Chicago, IL, USA
Abstract :
The dynamic behavior of concurrent systems can be modeled and analyzed using Petri nets. Many approaches have been proposed to analyze the properties of Petri nets. Among them, reachability analysis is a fundamental method for studying the dynamic properties of Petri nets. However, state space explosion has obstructed its applicability for analyzing large-scale systems. This paper presents a new method to attack state space explosion based on the concept of compositional verification. The strength of our method is in preserving the global information of Petri nets and a set of more effective condensation rules especially for tightly coupled modules (subnets). The current version of our method provides an efficient analysis for detecting deadlock states. An extension of our method for detecting reachable markings is also described
Keywords :
Petri nets; concurrency control; program verification; reachability analysis; systems analysis; Petri nets; compositional method; compositional verification; concurrent systems; condensation rules; condensed state-space verification; deadlock detection; dynamic behavior; dynamic properties; large-scale systems analysis; reachability analysis; reachable marking detection; state space explosion; tightly coupled modules; Explosions; Large-scale systems; Petri nets; Reachability analysis; State-space methods; System recovery;
Conference_Titel :
High-Assurance Systems Engineering Workshop, 1996. Proceedings., IEEE
Conference_Location :
Niagara on the Lake, Ont.
Print_ISBN :
0-8186-7629-9
DOI :
10.1109/HASE.1996.618571
