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

fYear

1996

fDate

21-22 Oct 1996

Firstpage

104

Lastpage

111

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;

fLanguage

English

Publisher

ieee

Conference_Titel

High-Assurance Systems Engineering Workshop, 1996. Proceedings., IEEE

Conference_Location

Niagara on the Lake, Ont.

Print_ISBN

0-8186-7629-9

Type

conf

DOI

10.1109/HASE.1996.618571

Filename

618571