This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Compact Petri Net Representation and Its Implications for Analysis
November 1996 (vol. 22 no. 11)
pp. 794-811

Abstract—This paper explores 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. This paper explores 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.

[1] 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.
[2] G. Andrews, “Paradigms for Process Interaction in Distributed Programs,” ACM Computing Surveys, Vol. 23, No. 1, Mar. 1991, pp. 49‐90.
[3] A.V. Aho, R. Sethi, and J.D. Ullman, Compilers, Principles, Techniques and Tools.New York: Addison-Wesley, 1985.
[4] 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.
[5] 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.
[6] A.T. Chamillard and L.A. Clarke, "Improving the Accuracy of Petri Net-Based Analysis of Concurrent Programs," Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 24-38, Jan. 1996.
[7] S.C. Cheung and J. Kramer, "Tractable Flow Analysis for Anomaly Detection in Distributed Programs," Proc. European Software Eng. Conf., vol. 717, Lecture Notes in Computer Science, pp. 283-300. Springer-Verlag, 1993.
[8] J.C. Corbett, "An Empirical Evaluation of Three Methods for Deadlock Analysis of Ada Tasking Programs," Software Eng. Notes, pp. 204-215, Proc. Int'l Symp. Software Testing and Analysis, Aug. 1994
[9] 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.
[10] M.B. Dwyer and L.A. Clarke, "Data Flow Analysis for Verifying Properties of Concurrent Programs," Software Eng. Notes, vol. 19, no. 5, pp. 62-75, Proc. ACM SIGSOFT Symp. Foundations of Software Eng., Dec. 1994.
[11] 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.
[12] E. Duesterwald and M.L. Soffa, "Concurrency Analysis in the Presence of Procedures Using a Data Flow Framework," Proc. ACM SIGSOFT Symp. Testing, Analysis and Verification, pp. 36-48, Oct. 1991.
[13] P. Godefroid and P. Wolper, "Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties," Proc. Third Workshop Computer Aided Verification, pp. 417-428, July 1991.
[14] 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.
[15] 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.
[16] S.P. Masticola and B.G. Ryder, "A Model of Ada Programs for Static Deadlock Detection in Polynomial Time," Proc. Workshop Parallel and Distributed Debugging, pp. 97-107, May 1991
[17] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[18] D. Mandrioli, R. Zicari, C. Ghezzi, and F. Tisato, "Modeling the Ada Task System by Petri Nets," Computer Languages, vol. 10, no. 1, pp. 43-61, 1985.
[19] J.L. Peterson, Petri Net Theory and the Modeling of Systems.Englewood Cliffs, N.J.: Prentice Hall, 1981.
[20] M. Pezzè, R.N. Taylor, and M. Young, "Graph Models for Reachability Analysis of Concurrent Programs," ACM Trans. Software Eng. and Methodology, vol. 4, no. 2, pp. 171-213, Apr. 1995.
[21] 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.
[22] S.M. Shatz, S. Tu, T. Murata, and S. Duri, "Theory and Application of Petri Net Reduction for Ada Tasking Deadlock Analysis," Technical Report, Dept. of Electrical Eng. and Computer Science, Univ. of Illi nois, Chicago, 1994.
[23] R.N. Taylor, "Complexity of Analyzing the Synchronization Structure of Concurrent Programs," Acta Informatica, vol. 19, pp. 57-84, 1983.
[24] R.N. Taylor, "A General-Purpose Algorithm for Analyzing Concurrent Programs," Comm. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[25] R.N. Taylor, F.C. Belz, L.A. Clarke, L.J. Osterweil, R.W. Selby, J.C. Wileden, A.L. Wolf, and M. Young, "Foundations for the Arcadia Environment Architecture," Proc. SIGSOFT '88: Third Symp. Software Development Environment, pp. 1-13, Nov. 1988. Published as ACM SIGPLAN Notices, vol. 24, no. 2 and as SIGSOFT Software Eng. Notes, vol. 13, no. 5, Nov. 1988.
[26] A. Valmari, "A Stubborn Attack on State Explosion," Proc. Second Workshop Computer Aided Verification, vol. 531, Lecture Notes in Computer Science, pp. 156-165. Springer-Verlag, 1991.
[27] M. Young, R.N. Taylor, D.L. Levine, K.A. Nies, and D. Brodbeck, "A Concurrency Analysis Tool Suite: Rationale, Design, and Preliminary Experience," ACM Trans.Software Eng. and Methodology, vol. 4, no. 1, pp. 64-106, Jan. 1995.
[28] 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.

Index Terms:
Software validation, reachability analysis, program representations, Petri nets, coarsened representations.
Citation:
Matthew B. Dwyer, Lori A. Clarke, "A Compact Petri Net Representation and Its Implications for Analysis," IEEE Transactions on Software Engineering, vol. 22, no. 11, pp. 794-811, Nov. 1996, doi:10.1109/32.553699
Usage of this product signifies your acceptance of the Terms of Use.