Improving the accuracy of Petri net-based analysis of concurrent programs

ABSTRACT

Spurious results are an inherent problem of most static analysis methods. These methods, in an effort to produce conservative results, overestimate the executable behavior of a program. Infeasible paths and imprecise alias resolution are the two causes of such inaccuracies. In this paper we present an approach for improving the accuracy of Petri net-based analysis of concurrent programs by including additional program state information in the Petri net. We present empirical results that demonstrate the improvements in accuracy and, in some cases, the reduction in the search space that result from applying this approach to concurrent Ada programs.

REFERENCES

• ABC+91: George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
• BCM+90: J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking' 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428-439, 1990.
• BDF92: Gianfranco Balbo, Susanna Donatelli, and Giuliana Franceschinis. Undenstanding parallel program behavior through petri net models. Journal of Parallel and Distributed Computing, 15(3):171-187, July 1992.
• Cha95: A. T. Chamillard, Improving Static Analysis Accuracy on Concurrent Ada Progra: Complexity Results and Empirical Findings, University of Massachusetts, Amherst, MA, 1995
• CK93: Shing-Chi Cheung , Jeff Kramer, Tractable Flow Analysis for Anomaly Detection in Distributed Programs, Proceedings of the 4th European Software Engineering Conference on Software Engineering, p.283-300, September 13-17, 1993
• CR81: Lori A. Clarke and Debra J. Richardson. Symbolic evaluation methods - implementations and applications. In Computer Program Testing, pages 65-102. Chandrasekaran and Radicchi, editors, North-Holland Publishing Company, 1981.
• Cor93: James C. Corbett, Identical tasks and counter variables in an integer programming-based approach to verification, Proceedings of the 7th international workshop on Software specification and design, December 06-07, 1993, Redondo Beach, California
• DBD+94: S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Application and experimental evaluation of state space reduction methods for deadlock analysis in Ada, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.340-380, Oct. 1994 [doi>10.1145/201024.201038]
• DC94: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• DCN95: Matthew B. Dwyer , Lori A. Clarke , Kari A. Nies, A compact Petri net representation for concurrent programs, Proceedings of the 17th international conference on Software engineering, p.147-157, April 24-28, 1995, Seattle, Washington, United States [doi>10.1145/225014.225028]
• GMO76: Harold N. Gabow, Shachindra N. Maheshwari, and Leon J. Osterweil. On two problems in the generation of program test paths. IEEE Transactions on Software Engineering, SE-2(3):227-231, September i976.
• HL85: D. Helmbold and D.C. Luckham. Debugging Ada tasking programs. IEEE Software, pages 47-57, March 1985.
• LC89: Douglas L. Long , Lori A. Clarke, Task interaction graphs for concurrency analysis, Proceedings of the 11th international conference on Software engineering, p.44-52, May 1989, Pittsburgh, Pennsylvania, United States [doi>10.1145/74587.74592]
• MR91: Stephen P. Masticola , Barbara G. Ryder, A model of Ada programs for static deadlock detection in polynomial times, Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, p.97-107, May 20-21, 1991, Santa Cruz, California, United States
• MR93: Stephen P. Masticola , Barbara G. Ryder, Non-concurrency analysis, Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.129-138, May 19-22, 1993, San Diego, California, United States
• Pet77: James L. Peterson, Petri Nets, ACM Computing Surveys (CSUR), v.9 n.3, p.223-252, Sept. 1977 [doi>10.1145/356698.356702]
• Pet81: James Lyle Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• RS90: John H. Reif , Scott A. Smolka, Data flow analysis of distributed communicating processes, International Journal of Parallel Programming, v.19 n.1, p.1-30, Feb. 1990 [doi>10.1007/BF01407862]
• SC88: S. M. Shatz , W. K. Cheng, A Petri net framework for automated analysis of Ada tasking behavior, Journal of Systems and Software, v.8 n.5, p.343-359, Dec. 1988 [doi>10.1016/0164-1212(88)90027-1]
• Tay83a: Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
• Tay83b: Richard Taylor. Complexity of analyzing the synchronization structure of concurrent programs. Acta Informatica, 19:57-84, 1983.
• TO80: Richard N. Taylor and Leon J. Osterweil. Anomaly detection in concurrent software by static data flow analysis. IEEE Transaction on Software Engineering, SE-6(3):265-277, May 1980.
• YT88: M. Young , R. M. Taylor, Combining Static Concurrency Analysis with Symbolic Execution, IEEE Transactions on Software Engineering, v.14 n.10, p.1499-1511, October 1988 [doi>10.1109/32.6195]
• YTF+89: M. Young , R. Taylor , K. Forester , D. Brodbeck, Integrated concurrency analysis in a software development enviornment, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.200-209, December 13-15, 1989, Key West, Florida, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

General Terms:
Design, Experimentation, Measurement, Performance, Theory