This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent-Software Analysis
May 1994 (vol. 20 no. 5)
pp. 325-336

Petri nets have been proposed as a promising tool for modeling and analyzing concurrent-software systems such as Ada programs and communication protocol software. Among analysis techniques available for Petri nets, the most general approach is to generate all possible states (markings) of the system in a form of a so-called reachability graph. However, this conventional reachability graph approach is inefficient or intractable, even for a bounded Petri net, due to state explosion in many practical applications. To cope with this problem, this paper proposes a method for constructing a hierarchically organized state space called the hierarchical reachability graph (HRG). Using the HRG, we obtain necessary and sufficient conditions for reachability and deadlock, as well as algorithms to test whether a given state or marking is reachable from the initial state and whether there is a deadlock state (a state with no successor states)

[1] T. Murata, B. Shenker, and S. M. Shatz, "Detection of Ada static deadlocks using Petri net invariants,"IEEE Trans. Software Eng., vol. 15, pp. 314-326, Mar. 1989.
[2] S. M. Shatz and W. K. Cheng, "A Petri net framework for automated static analysis of Ada tasking behavior,"J. Syst. Software, vol. 8, pp. 343-359, 1988.
[3] D. Mandrioli, R. Zicari, C. Ghezzi, and F. Tisato, "Modeling the Ada task system by Petri nets,"Comput. Lang., vol. 10, no. 1, 1985.
[4] T. Suzuki, S. M. Shatz, and T. Murata, "A protocol modeling and verification approach based on a specification language and Petri nets,"IEEE Trans. Software Eng., vol. 16, pp. 523-536, May 1990.
[5] M. Diaz, "Modeling and analysis of communication and cooperation protocols using Petri net based models,"Comput. Networks, vol. 6, pp. 419-441, Dec. 1982.
[6] G. R. Wheeler, M. C. Wilbur-Ham, J. Billington, and J. A. Gilmour, "Protocol analysis using Numerical Petri Nets,"Advances in Petri Nets 1985, (Lecture Notes in Computer Science, vol. 222). Berlin: Springer-Verlag, 1986, pp. 435-452.
[7] A. Valmari, "Compositional state space generation,"Proc. 11th Int. Conf. Application and Theory of Petri Nets, 1990, pp. 43-62.
[8] A. Valmari, "A stubborn attack on state explosion," inComputer-Aided Verification '90(Series in Discrete Mathematics and Theoretical Computer Sci., vol. 3), E. M. Clarke and R. P. Kurshan, Eds. Providence, RI: Amer. Math. Soc., 1991, pp. 25-41.
[9] E. T. Morgan and R. R. Razouk, "Interactive state-space analysis of concurrent systems,"IEEE Trans. Software Eng., vol. SE-13, pp. 1080-1091, Oct. 1987.
[10] R. Janicki and M. Kounty, "Optimal simulations, nets and reachability graphs," Tech. Rep. 91-09, MacMaster Univ., Hamilton, ON, Canada.
[11] T. Murata, "Petri nets: Properties, analysis, and applications,"Proc. IEEE, vol. 77, no. 4, pp. 541-580, Apr. 1989.
[12] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[13] J. A. Brookes and J. W. Klop, "Process algebra for synchronous communication,"Inform. Control, vol. 60, pp. 109-137, 1984.
[14] M. Tiusanen and T. Murata, "Models for static analysis of Ada tasking programs," Tech. Rep. 92-7, Dept. of Elec. Eng. and Comput. Sci., Univ. of Ill., Chicago, 1992.
[15] W. J. Yeh and M. Young, "Compositional reachability analysis using process algebra," inProc. Symp. on Software Test., Analysis, and Verification (TAV4), (Victoria, BC, Can.), Oct. 1991, pp. 49-59.
[16] A. Valmari and M. Tienari, "An improved failure equivalence for finite-state systems with a reduction algorithm," inProtocol Specification, Testing, and Verification XI, B. Jonson, J. Parrow, and B. Pehrson, Eds. Amsterdam: North-Holland, 1991, pp. 3-18.
[17] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe, "A theory of communicating sequential processes,"J. ACM, vol. 31, no. 3, pp. 560-599, July 1984.
[18] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[19] R. Milner,Communication and Concurrency, Englewood Cliffs, NJ: Prentice-Hall, 1989.
[20] T. Bolognesi and E. Brinksma, "Introduction to the ISO specification language LOTOS," inThe Formal Description Technique LOTOS. Amsterdam: North-Holland, 1989, pp. 23-73.
[21] R. Kaivola and A. Valmari, "Using truth-preserving reductions to improve the clarity of Kripke-models," Proceedings ofCONCUR '91, Lecture Notes in Comput. Sci. 527, J. C. M. Baeten and J. F. Groote, Eds. Berlin: Springer-Verlag, 1991, pp. 361-375.
[22] R. Kaivola and A. Valmari, "The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic,"Procs. CONCUR'92, Lecture Notes in Comput. Sci. 630, W. R. Cleaveland, Ed. Berlin: Springer-Verlag, 1992, pp. 207-221.
[23] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[24] D. L. Long and L. A. Clarke, "Task interaction graphs for concurrency analysis," inProc. 11th Int. Conf. on Software Eng.(Pittsburgh, PA), May 1989.

Index Terms:
Petri nets; state-space methods; multiprocessing programs; software engineering; hierarchical systems; hierarchical reachability graph; bounded Petri nets; concurrent-software analysis; Ada programs; communication protocol software; markings; state explosion; efficiency; tractability; hierarchically organized state space; deadlock state; successor states
Citation:
M. Notomi, T. Murata, "Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent-Software Analysis," IEEE Transactions on Software Engineering, vol. 20, no. 5, pp. 325-336, May 1994, doi:10.1109/32.286423
Usage of this product signifies your acceptance of the Terms of Use.