Using symbolic execution for verification of Ada tasking programs

ABSTRACT

A method is presented for using symbolic execution to generate the verification conditions required for proving correctness of programs written in a tasking subset of Ada. The symbolic execution rules are derived from proof systems that allow tasks to be verified independently in local proofs, which are then checked for cooperation. The isolation nature of this approach to symbolic execution of concurrent programs makes it better suited to formal verification than the more traditional interleaving approach, which suffers from combinatorial problems. The criteria for correct operation of a concurrent program include partial correctness, as well as more general safety properties, such as mutual exclusion and freedom from deadlock.

REFERENCES

• 1: Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
• 2: BARRINGER, H., AND MEARNS, {. Axioms and proof rules for Ada tasks. In Proc. IEE 129 (1982), no. pt. E.
• 3: BRAND, D., AND JOYNER, W. H. JR. Verification of protocols using symbolic execution. Comput. Networks 2 (1978), 351-360.
• 4: Laura K. Dillion, An isolation approach to symbolic execution-based verification of Ada tasking programs, Journal of Systems and Software, v.14 n.3, p.183-198, March 1991 [doi>10.1016/0164-1212(91)90065-E]
• 5: Laura K. Dillon, Verifying General Safety Properties of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.16 n.1, p.51-63, January 1990 [doi>10.1109/32.44363]
• 6: DILLON, L. K., KEMMERER, R. A., AND HARRISON, r.J. An experience with two symbolic execution-based approaches to formal verification of Ada tasking programs. In Proceedings of the 2nd Workshop of Software Testing, Verification, and Analysis (Washington, DC, July 1988). IEEE Computer Society Press, New York, 1988, 114-122.
• 7: FLOYD, R.W. Assigning meanings to programs. In Proceedings of the American Mathematical Society Symposia in Applied Mathematics 19 (1967), 19-31.
• 8: Rob Gerth , Willem P. De Roever, A proof system for concurrent ADA programs, Science of Computer Programming, v.4 n.2, p.159-204, August 1984 [doi>10.1016/0167-6423(84)90018-2]
• 9: Donald I. Good , Richard M. Cohen , James Keeton-Williams, Principles of proving concurrent programs in Gypsy, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.42-52, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567757]
• 10: Sidney L. Hantler , James C. King, An Introduction to Proving the Correctness of Programs, ACM Computing Surveys (CSUR), v.8 n.3, p.331-353, Sept. 1976 [doi>10.1145/356674.356677]
• 11: HARRISON, L. J., AND KEMMERER, R.A. An interleaving symbolic execution approach for the formal verification of Ada programs with tasking. In Proceedings of the 3rd International IEEE Conference on Ada Applications and Environments (Washington, DC, May 1988), 15-26.
• 12: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 13: KEMMERER, R. A., AND ECKMANN, S. V. UNISEX: A UNix-based symbolic EXecutor for Pascal. Softw. Pract. Exper. 15, 5 (May 1985), 439-457.
• 14: KNIGHT, J. C., AND GRINE, V.S. Symbolic execution of concurrent Ada programs. Tech. Rep., Department of Computer Science, University of Virginia, Charlottesville.
• 15: LAMPORT, r. The "Hoare logic" of concurrent programs. Acta Inf. 14 (1980), 21-37.
• 16: Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984 [doi>10.1145/2993.357247]
• 17: LUCKHAM, D. C., HELMBOLD, D. P., MELDAL, S., BRYAN, D. L., AND HABERLER, M.A. Task sequencing language for specifying distributed Ada systems: TSL-1. Tech. Rep., Program Analysis and Verification Group, Computer Systems Laboratory, Stanford University, Stanford, CA, 1987.
• 18: LUCKHAM, D. C., AND VON HENKE, F.W. An overview of Anna, a specification language for Ada. IEEE Softw. (Mar. 1985), 9-22.
• 19: M1SRA, J., AND CHANDY, $. M. Proofs of networks and processes. IEEE Trans. Softw. Eng. SE-7, 4 (July 1981), 417-426.
• 20: Van Nguyen , Alan Demers , David Gries , Susan Owicki, A model and temporal proof system for networks of processes, Distributed Computing, v.1 n.1, p.7-25, Jan. 1986 [doi>10.1007/BF01843567]
• 21: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 22: YOUNG, M., AND TAYLOR, R. $. Combining static concurrency analysis with symbolic execution. In Proceedings of the Workshop on Software Testing ( July 1986).

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Symbolic execution
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Ada

General Terms:
Languages, Verification