This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Application of Petri Net Reduction for Ada Tasking Deadlock Analysis
December 1996 (vol. 7 no. 12)
pp. 1307-1322

Abstract—As part of our continuing research on using Petri nets to support automated analysis of Ada tasking behavior, we have investigated the application of Petri net reduction for deadlock analysis. Although reachability analysis is an important method to detect deadlocks, it is in general inefficient or even intractable. Net reduction can aid the analysis by reducing the size of the net while preserving relevant properties. We introduce a number of reduction rules and show how they can be applied to Ada nets, which are automatically generated Petri net models of Ada tasking. We define a reduction process and a method by which a useful description of a detected deadlock state can be obtained from the reduced net's information. A reduction tool and experimental results from applying the reduction process are discussed.

[1] J. Reif and S. Smolka, “The Complexity of Reachability in Distributed Communicating Processes,” Acta Informatica, vol. 25, no. 3, pp. 333–354, 1988.
[2] T. Rauchle and S. Toueg, "Exposure to Deadlock for Communicating Processes is Hard to Detect," Information Processing Letters, vol. 21, pp. 63-68, 1978.
[3] R.N. Taylor, "Complexity of Analyzing the Synchronization Structure of Concurrent Programs," Acta Informatica, vol. 19, pp. 57-84, 1983.
[4] R.N. Taylor, "A General-Purpose Algorithm for Analyzing Concurrent Programs," Comm. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[5] D.L. Long and L.A. Clarke, "Task Interaction Graphs for Concurrency Analysis," Proc. 11th Int'l Conf. Software Eng., pp. 44-52, May 1989.
[6] S.M. Shatz and W.K. Cheng, "A Petri Net Framework For Automated Static Analysis of Ada Tasking Behavior," J. Systems and Software, vol. 8, pp. 343-359, Dec. 1988.
[7] G. Avrunin and J. Wileden, "Describing and Analyzing Distributed Software System Designs," ACM Trans. Programming Languages and Systems, vol. 7, no. 3, pp. 380-403, July, 1985.
[8] G.S. Avrunin, U.A. Buy, J.C. Corbett, L.K. Dillon, and J.C. Wileden, "Automated Analysis of Concurrent Systems with the Constrained Expression Toolset," IEEE Trans. Software Eng. vol. 17, no. 11, pp. 1204-1222, Nov. 1991.
[9] T. Murata, B. Shenker, and S.M. Shatz, "Detection of Ada Static Deadlocks Using Petri Net Invariants," IEEE Trans. Software Eng., vol. 15, no. 3, pp. 314-326, Mar. 1989.
[10] S.M. Shatz, K. Mai, C. Black, and S. Tu, "Design and Implementation of a Petri Net Based Toolkit for Ada Tasking Analysis," IEEE Trans. Parallel and Distributed Systems vol. 1, no. 4, pp. 424-441, Oct. 1990.
[11] C. Black, S.M. Shatz, and S. Upp, "TQL: A Tasking Query Language for Concurrent Program Analysis," Proc. 12th Int'l Conf. Distributed Computing Systems, pp. 382-389,Yokohama, Japan, June 1992.
[12] A. Blakemore and G. Schebella, "Tools for Analyzing Dynamic Properties of System and Software Designs," Proc. IFIP XI Congress,San Francisco, 1989.
[13] G.M. Karam and R.J. Buhr, "Starvation and Critical Race Analyzers For Ada," IEEE Trans. Software Eng., vol. 16, no. 8, pp. 829-843, 1990.
[14] W.J. Yeh and M. Young, "Compositional Reachability Analysis Using Process Algebra," Proc. ACM SIGSOFT Symp. Testing, Analysis and Verification, pp. 49-59, Oct. 1991.
[15] W.J. Yeh, "Controlling State Explosion in Reachability Analysis," PhD Dissertation, Dept. of Computer Science, Purdue Univ., Aug. 1993.
[16] J.C. Corbett, "Identical Tasks and Counter Variables in an Integer Programming-Based Approach to Verification," Proc. Seventh Int'l ACM Workshop Software Specification and Design, pp. 100-109, Dec. 1993.
[17] M.B. Dwyer, L.A. Clarke, and K.L. Nies, "A Compact Petri Net Representation for Concurrent Programs," Proc. 17th Int'l Conf. Software Eng., pp. 147-158, Apr. 1995.
[18] R. Enders, T. Filkorn, and D. Taubner, "Generating BDDs for Symbolic Model Checking in CCS," Proc. Workshop Computer Aided Verification (CAV), pp. 263-278, 1991.
[19] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 1020States and Beyond," Proc. IEEE Symp. Logic in Computer Science, pp. 428-439, 1990.
[20] A. Valmari, "A Stubborn Attack on State Space Explosion," Proc. Workshop Computer-Aided Verification, LNCS 531, pp. 156-165.New York: Springer-Verlag, 1991. Also in Formal Methods in System Design. Kluwer Academic Publishers, vol. 1, 1992, pp. 297-322.
[21] P. Godefroid and P. Wolper, "Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties," Formal Methods in System Design, pp. 149-164, Apr. 1993.
[22] P.H. Starke, "Reachability Analysis of Petri Nets Using Symmetries," Systems Analysis, Modeling, and Simulation, vol. 8, pp. 293-303, 1991.
[23] S. Duri, U. Buy, R. Devarapalli, and S.M. Shatz, "Application and Experimental Evaluation of State Space Reduction Methods for Deadlock Analysis in Ada," ACM Trans. Software Eng. and Methodology, pp. 340-380, vol. 3, no. 4, Oct. 1994.
[24] J.L. Peterson, Petri Net Theory and the Modeling of Systems.Englewood Cliffs, N.J.: Prentice Hall, 1981.
[25] K. Gostelow, V. Cerf, G. Estrin, and S. Volansky, "Proper Termination of Flow-of Control in Programs Involving Concurrent Processes," Proc. ACM Ann. Conf., vol. II, pp. 742-754,Boston, Aug. 1972.
[26] G. Berthelot, "Checking Properties of Nets Using Transformations," Advances in Petri Nets, vol. 222, Lecture Notes in Computer Science, pp. 19-40. Springer-Verlag, 1987.
[27] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[28] U.S. Dept. of Defense, Reference Manual for the Ada Programming Language, ANSI/MIL-STD-1815A-1983, Feb.17, 1983.
[29] D. Helmbold and D. Luckham, "Debugging Ada Tasking Programs," IEEE Software, vol. 2, no. 2, pp. 47-57, Mar. 1985.
[30] E.T. Morgan and R.R. Razouk, "Interactive State-Space Analysis of Concurrent Systems," IEEE Trans. on Software Eng., vol. 13, no. 10, pp. 1080-1091, 1987.
[31] M. Young, R.N. Taylor, K. Forester, and D. Brodbeck, "Integrated Concurrency Analysis in a Software Development Environment," R.A. Kemmerer, ed., Proc. Third Symp. Software Testing, Analysis and Verification, ACM SIGSOFT, pp. 200-209, 1989. Appeared as Software Engineering Notes, vol. 14, no. 8.
[32] M. Young, R. Taylor, D. Levine, K. Forester, and D. Brodbeck, "A Concurrency Analysis Tool Suite: Rationale, Design, and Preliminary Experience," Technical Report TR-128-P, Software Eng. Research Center, Purdue Univ., Oct. 1992.
[33] S. Duri, U. Buy, R. Devarapalli, and S.M. Shatz, "Using State Space Reduction Methods for Deadlock Analysis in Ada Tasking," Proc. Int'l Symp. Software Testing and Analysis (ISSTA), Ostrand and Weyuker, eds., [37], pp. 51-60,New York: ACM Press, June 1993.
[34] A. Valmari and M. Tienari, "An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm," Proc. 11th IFIP Working Group 6.1 Symp. Protocol Specification, Testing and Verification. pp. 3-18.Stockholm, Sweden: North-Holland, June 1991.

Index Terms:
Ada tasking, deadlock analysis, Petri nets, net reduction, reachability analysis, concurrent software.
Citation:
Sol M. Shatz, Shengru Tu, Tadao Murata, Sastry Duri, "An Application of Petri Net Reduction for Ada Tasking Deadlock Analysis," IEEE Transactions on Parallel and Distributed Systems, vol. 7, no. 12, pp. 1307-1322, Dec. 1996, doi:10.1109/71.553301
Usage of this product signifies your acceptance of the Terms of Use.