Experiments in automated analysis of concurrent software systems

ABSTRACT

It is unlikely that any single approach to analysis of concurrent software systems will meet all the needs of software developers throughout the development process. Thus, experimental evaluation of different analysis techniques is needed to determine their relative strengths and practical limitations. Such evaluation requires automated tools implementing the analysis techniques. This paper describes a prototype toolset automating the constrained expression approach to the analysis of concurrent software systems. The results of preliminary experiments with the toolset are reported and the implications of these experiments are discussed.

REFERENCES

• 1: S. Avery. A tool for producing constrained expression representations of CEDL designs. Software Development Laboratory Memo 89-2, Department of Computer and Information Science, University of Massachusetts, 1989.
• 2: George S. Avrunin, Experiments in Constrained Expression Analysis, University of Massachusetts, Amherst, MA, 1988
• 3: G. S. Avrunin and U. Buy. An inequality generator for constrained expression analysis. In preparation.
• 4: George S. Avrunin , Laura K. Dillon , Jack C. Wileden, Constrained Expression Analysis of Real-Time Systems, University of Massachusetts, Amherst, MA, 1989
• 5: 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
• 6: George S. Avrunin , Jack C. Wileden, Describing and analyzing distributed software system designs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.380-403, July 1985 [doi>10.1145/3916.3989]
• 7: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 8: R. H. Carver and K.-C. Tai. Detection of synchronization errors in concurrent software by semantics-based analysis. Preprint, 1988.
• 9: L. A. Cla.rke, J. C. Wileden, and A. L. Wolf. GRAPHITE: A meta-tool for Ada environment development. In Proceedings of 2nd International Conference on Ada Applications and Environments, pages 81-90, April 1986.
• 10: R. J. Dakin. A tree search algorithm for mixed integer programming problems. Computer Journal, 8:250-255, 1965.
• 11: Laura K. Dillon, Analysis of distributed systems using constrained expressions (concurrent systems), 1984
• 12: L. K. Dillon. Overview of the constrained expression design language. Technical Report TRCS86-21, Department of Computer Science, University of California, Santa Barbara, October 1986.
• 13: 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]
• 14: L. K. Dillon and G. Walden. A prototype constraint eliminator for constrained expression representations. In preparation.
• 15: M. Greenberg and S. Avery. A behavior generator. Software Development Laboratory Memo 89-1, Department of Computer and Information Science, University of Massachusetts, 1988.
• 16: A. Nico Habermann, Synchronization of communicating processes, Communications of the ACM, v.15 n.3, p.171-176, March 1972 [doi>10.1145/361268.361277]
• 17: D. Helmbold and D. Luckham. Debugging Ada tasking programs. IEEE Software, 2(2):47-57, March 1985.
• 18: A. H. Land and A. G. Doig. An automatic method for solving discrete programming problems. Econometrica, 28:497-520, 1960.
• 19: Ailsa H. Land , S. Powell, FORTRAN Codes for Mathematical Programming: Linear, Quadratic and Discrete, John Wiley & Sons, Inc., New York, NY, 1973
• 20: P. Lauer, P. Torrigiani, and M. Shields. COSY: A system specification language based on paths and processes. Acta Informatica, 12(2):451-503, 1979.
• 21: W. E. Riddle. An approach to software system behavior modeling. Computer Languages, 4:29-47, 1979.
• 22: M. A. Saunders. MINOS system manual. Technical Report SOL 77-31, Stanford University, Department of Operations Research, 1977.
• 23: 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
• 24: J. C. Wileden and G. S. Avrunin. Toward automating analysis support for developers of distributed software. In Proceedings of the Eighth International Conference on Distributed Computing Systems, pages 350-357. IEEE Computer Society Press, June 1988.
• 25: J. C. Wileden, A. L. Wolf, W. R. Rosenblatt, and P. L. Tarr. Specification level interoperability. Submitted.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

General Terms:
Experimentation, Verification