This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Detection of Ada Static Deadlocks Using Petri Net Invariants
March 1989 (vol. 15 no. 3)
pp. 314-326

A method is presented for detecting deadlocks in Ada tasking programs using structural; and dynamic analysis of Petri nets. Algorithmic translation of the Ada programs into Petri nets which preserve control-flow and message-flow properties is described. Properties of these Petri nets are discussed, and algorithms are given to analyze the nets to obtain information about static deadlocks that can occur in the original programs. Petri net invariants are used by the algorithms to reduce the time and space complexities associated with dynamic Petri net analysis (i.e. reachability graph generation).

[1] I. C. Pyle,The Ada Programming Language. London, UK: Prentice-Hall, 1981.
[2] N. Gehani,An Advanced Introduction Including Reference Manual for the Ada Programming Language. Englewood Cliffs, NJ: Prentice-Hall, 1984.
[3] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[4] S. German, "Monitoring for deadlocks and blocking in Ada tasking,"IEEE Trans. Software Eng., vol. SE-10, Nov. 1984.
[5] B. Shenker, "Using Petri nets for automated detection of static deadlocks in Ada programs," Master's thesis, Dep. Elec. Eng. Comput. Sci., Univ. Illinois, Chicago, IL, Sept. 1985.
[6] T. Murata, "Modeling and analysis of concurrent systems," inHandbook of Software Engineering, C. R. Vick and C. V. Ramamoorthy, Eds. New York: Van Nostrand Reinhold, 1983, ch. 3.
[7] 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.
[8] J. Martinez and M. Silva, "A simple and fast algorithm to obtain all invariants of a generalised Petri net,"Second European Workshop on Application and Theory of Petri Nets, 1982, pp. 301-310.
[9] E. Horowitz and S. Sahni,Fundamentals of Data Structures. Rockville, MD: Computer Science Press, 1983.
[10] R. N. Taylor and T. A. Standish, "Steps to an advanced Ada programming environment,"IEEE Trans. Software Eng., vol. SE-11, no. 3, pp. 302-310, Mar. 1985.
[11] D. Mandrioli, R. Zicari, C. Ghezzi, and F. Tisato, "Modeling the Ada task system by Petri nets,"Comput. Lang., vol. 10, no. 1, 1985.

Index Terms:
Ada static deadlocks; Petri net invariants; Ada tasking programs; control-flow; message-flow; complexities; Ada; computational complexity; concurrency control; Petri nets; program testing; system recovery.
Citation:
T. Murata, B. Shenker, S.M. Shatz, "Detection of Ada Static Deadlocks Using Petri Net Invariants," IEEE Transactions on Software Engineering, vol. 15, no. 3, pp. 314-326, March 1989, doi:10.1109/32.21759
Usage of this product signifies your acceptance of the Terms of Use.