
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
M. Notomi, T. Murata, "Hierarchical Reachability Graph of Bounded Petri Nets for ConcurrentSoftware Analysis," IEEE Transactions on Software Engineering, vol. 20, no. 5, pp. 325336, May, 1994.  
BibTex  x  
@article{ 10.1109/32.286423, author = {M. Notomi and T. Murata}, title = {Hierarchical Reachability Graph of Bounded Petri Nets for ConcurrentSoftware Analysis}, journal ={IEEE Transactions on Software Engineering}, volume = {20}, number = {5}, issn = {00985589}, year = {1994}, pages = {325336}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.286423}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Hierarchical Reachability Graph of Bounded Petri Nets for ConcurrentSoftware Analysis IS  5 SN  00985589 SP325 EP336 EPD  325336 A1  M. Notomi, A1  T. Murata, PY  1994 KW  Petri nets; statespace methods; multiprocessing programs; software engineering; hierarchical systems; hierarchical reachability graph; bounded Petri nets; concurrentsoftware analysis; Ada programs; communication protocol software; markings; state explosion; efficiency; tractability; hierarchically organized state space; deadlock state; successor states VL  20 JA  IEEE Transactions on Software Engineering ER   
Petri nets have been proposed as a promising tool for modeling and analyzing concurrentsoftware 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 socalled 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. 314326, 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. 343359, 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. 523536, May 1990.
[5] M. Diaz, "Modeling and analysis of communication and cooperation protocols using Petri net based models,"Comput. Networks, vol. 6, pp. 419441, Dec. 1982.
[6] G. R. Wheeler, M. C. WilburHam, 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: SpringerVerlag, 1986, pp. 435452.
[7] A. Valmari, "Compositional state space generation,"Proc. 11th Int. Conf. Application and Theory of Petri Nets, 1990, pp. 4362.
[8] A. Valmari, "A stubborn attack on state explosion," inComputerAided 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. 2541.
[9] E. T. Morgan and R. R. Razouk, "Interactive statespace analysis of concurrent systems,"IEEE Trans. Software Eng., vol. SE13, pp. 10801091, Oct. 1987.
[10] R. Janicki and M. Kounty, "Optimal simulations, nets and reachability graphs," Tech. Rep. 9109, MacMaster Univ., Hamilton, ON, Canada.
[11] T. Murata, "Petri nets: Properties, analysis, and applications,"Proc. IEEE, vol. 77, no. 4, pp. 541580, 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. 109137, 1984.
[14] M. Tiusanen and T. Murata, "Models for static analysis of Ada tasking programs," Tech. Rep. 927, 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. 4959.
[16] A. Valmari and M. Tienari, "An improved failure equivalence for finitestate systems with a reduction algorithm," inProtocol Specification, Testing, and Verification XI, B. Jonson, J. Parrow, and B. Pehrson, Eds. Amsterdam: NorthHolland, 1991, pp. 318.
[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. 560599, July 1984.
[18] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: SpringerVerlag, 1980.
[19] R. Milner,Communication and Concurrency, Englewood Cliffs, NJ: PrenticeHall, 1989.
[20] T. Bolognesi and E. Brinksma, "Introduction to the ISO specification language LOTOS," inThe Formal Description Technique LOTOS. Amsterdam: NorthHolland, 1989, pp. 2373.
[21] R. Kaivola and A. Valmari, "Using truthpreserving reductions to improve the clarity of Kripkemodels," Proceedings ofCONCUR '91, Lecture Notes in Comput. Sci. 527, J. C. M. Baeten and J. F. Groote, Eds. Berlin: SpringerVerlag, 1991, pp. 361375.
[22] R. Kaivola and A. Valmari, "The weakest compositional semantic equivalence preserving nexttimeless linear temporal logic,"Procs. CONCUR'92, Lecture Notes in Comput. Sci. 630, W. R. Cleaveland, Ed. Berlin: SpringerVerlag, 1992, pp. 207221.
[23] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362376, 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.