Combining structural and symbolic methods for the verification of concurrent systems

Author

Cortadella, Jordi

Author_Institution

Dept. of Software, Univ. Politecnica de Catalunya, Barcelona, Spain

fYear

1998

fDate

23-26 Mar 1998

Firstpage

2

Lastpage

7

Abstract

The contributions during the last few years on the structural theory of Petri nets can now be applied to formal verification. The structural theory provides methods to find efficient encoding schemes for symbolic representations of the reachable markings. It also provides approximations of the state space that allow one to alleviate many bottlenecks in the calculation of the reachability set by breadth or depth first search algorithms. The paper reviews some of the results on the structural theory and explains how they can be incorporated in a model checking verification framework for concurrent systems

Keywords

Petri nets; parallel programming; program verification; tree searching; Petri nets; breadth first search; concurrent systems verification; depth first search algorithms; efficient encoding schemes; formal verification; model checking verification framework; reachability set; reachable markings; state space approximations; structural theory; symbolic methods; symbolic representations; Concurrent computing; Databases; Encoding; Explosions; Interleaved codes; Logic; Petri nets; Skeleton; State-space methods;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 1998. Proceedings., 1998 International Conference on

Conference_Location

Fukushima

Print_ISBN

0-8186-8350-3

Type

conf

DOI

10.1109/CSD.1998.657533

Filename

657533