Integrated concurrency analysis in a software development enviornment

ABSTRACT

The inherent difficulties of analyzing concurrent software make reliance on a single technique or a single monolithic tool unsatisfactory. A better approach is to apply multiple analysis and verification techniques by coordinating the activities of a variety of small tool components. We describe how this approach has shaped the design of a set of tool components to support concurrency analysis in the Arcadia-1 software development environment. Implementation and experience with key components is described.

REFERENCES

• ADWR86: G S Avrunin , L K Dillon , J C Wileden , W E Riddle, Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems, IEEE Transactions on Software Engineering, v.12 n.2, p.278-292, Feb. 1986
• Apt83: Krzysztof R. Apt, A Static Analysis of CSP Programs, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.1-17, June 06-08, 1983
• CBES85: E. M. Clarke , M. C. Browne , E. A. Emersonn , A. P. Sistla, Using temporal logic for automatic verification of finite state systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• CES86: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• CRZ88: Lori A. Clarke , Debra J. Richardson , Steven J. Zeil, TEAM: a support environment for testing, evaluation, and analysis, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.153-162, November 28-30, 1988, Boston, Massachusetts, United States
• DAW88: Laura K. Dillon , George S. Avrunin , Jack C. Wileden, Constrained expressions: toward broad applicability of analysis methods for distributed software systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.374-402, July 1988 [doi>10.1145/44501.44502]
• GHL82: Steven M. German, David P. Helmbold, and David C. Luckham. Monitoring for deadlocks in Ada tasking. In Proceedings of the AdaTEC Conference on Ada, pages 10-25, Arlington, VA, October 1982.
• JRT86: T A Joseph , T Räuchle , S Toueg, State machines and assertions: An integrated approach to modeling and verification of distributed systems, Science of Computer Programming, v.7 n.1, p.1-22, July 1986
• Lad79: Richard E. Ladner, The complexity of problems in systems of communicating sequential processes (Extended Abstract), Proceedings of the eleventh annual ACM symposium on Theory of computing, p.214-223, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804415]
• Lam88: Leslie Lamport, Control predicates are better than dummy variables for reasoning about program control, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.267-281, April 1988 [doi>10.1145/42190.42348]
• 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]
• MR87: E. Timothy Morgan , Rami R. Razouk, Interactive state-space analysis of concurrent systems, IEEE Transactions on Software Engineering, v.13 n.10, p.1080-1091, October 1, 1987 [doi>10.1109/TSE.1987.232850]
• OG76: Susan Owicki and David Gries. An axiomatic proof technique for parallel programs. Acta Infomotica, 6(4):319- 340, 1976.
• Pet81: James Lyle Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• Raz87: Rami R. Fbazouk. A guided tour of P-NUT. Technical Report 86-25, University of California, 1987.
• Smo84: Scott Allen Smolka, Analysis of communicating finite-state processes, 1984
• Tai85: Kuo-Chung Tai, Reproducible testing of concurrent Ada programs, Proceedings of the second conference on Software development tools, techniques, and alternatives, p.114-121, December 1985, San Francisco, California, United States
• Tay83a: Richard N. Taylor. Complexity of analyzing the synchro nization structure of concurrent programs. Acto Infornaatica, 19:57-84, 1983.
• Tay83b: 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]
• Tay84: Richard N. Taylor, Analysis of concurrent software by cooperative application of static and dynamic techniques, Proc. of a symposium on Software validation: inspection-testing-verification-alternatives, p.127-137, October 1984, Darmstadt, Germany
• TBC+88: Richard N. Taylor , Frank C. Belz , Lori A. Clarke , Leon Osterweil , Richard W. Selby , Jack C. Wileden , Alexander L. Wolf , Michael Young, Foundations for the Arcadia environment architecture, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.1-13, November 28-30, 1988, Boston, Massachusetts, United States
• TK86: Richard N. Taylor and Cheryl D. Kelly. Structural testing of concurrent programs. In Proceedings of the Workshop on Software Testing, pages 164-169, Banff, Canada, July 1986.
• Wam85: Gordon Kent Wampler. Static concurrency analysis of Ada programs. Master's thesis, University of California, Irvine, 1985.
• Wei88: Stewart N. Weiss. A formal framework for the study of concurrent program testing. In Proceedings of the Second Workshop on Software Testing, Analysis, and Vertfication, pages 106-113, Banff, Canada, July 1988. ACM/SIGSOFT and IEEE-CS Software Engineering Technical Committee.
• WWFT88: Jack C. Wileden , Alexander L. Wolf , Charles D. Fisher , Peri L. Tarr, Pgraphite: an experiment in persistent typed object management, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.130-142, November 28-30, 1988, Boston, Massachusetts, United States
• You88: Michal Young. How to leave out details: Error-preserving abstractions of state-space models. In Proceedings of the Second Workshop on Software Testing, Analysis, and Verification, pages 63-70, Banff, Canada, July 1988.
• 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]
• ZE88: S. J. Zeil , E. C. Epp, Interpretation in a tool-fragment environment, Proceedings of the 10th international conference on Software engineering, p.241-248, April 11-15, 1988, Singapore

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Debugging aids

General Terms:
Design, Reliability, Verification