Title :
A compact Petri net representation and its implications for analysis
Author :
Dwyer, Matthew B. ; Clarke, Lori A.
Author_Institution :
Dept. of Comput. & Inf. Sci., Kansas State Univ., Manhattan, KS, USA
fDate :
11/1/1996 12:00:00 AM
Abstract :
We explore a property-independent, coarsened, multilevel representation for supporting state reachability analysis for a number of different properties. This multilevel representation comprises a reachability graph derived from a highly optimized Petri net representation that is based on task interaction graphs and associated property-specific summary information. This highly optimized representation reduces the size of the reachability graph but may increase the cost of the analysis algorithm for some types of analyses. We explore this tradeoff. To this end, we have developed a framework for checking a variety of properties of concurrent programs using this optimized representation and present empirical results that compare the cost to an alternative Petri net representation. In addition, we present reduction techniques that can further improve the performance and yet still preserve analysis information. Although worst-case bounds for most concurrency analysis techniques are daunting, we demonstrate that the techniques that we propose significantly broaden the applicability of reachability analyses
Keywords :
Petri nets; optimisation; parallel programming; program verification; programming theory; reachability analysis; software cost estimation; Petri net representation; concurrency analysis techniques; concurrent program property checking; cost; optimization; performance; property-independent multilevel representation; property-specific summary information; reachability graph; reduction techniques; software validation; state reachability analysis; task interaction graphs; worst-case bounds; Algorithm design and analysis; Costs; Electronic mail; Failure analysis; Information analysis; Petri nets; Production systems; Software engineering; Software systems; System recovery;
Journal_Title :
Software Engineering, IEEE Transactions on