This Article 
 Bibliographic References 
 Add to: 
Verifying General Safety Properties of Ada Tasking Programs
January 1990 (vol. 16 no. 1)
pp. 51-63

The isolation approach to symbolic execution of Ada tasking programs provides a basis for automating partial correctness proofs. The strength of this approach lies in its isolation nature; tasks are symbolically executed and verified independently, and then checked for cooperation where interference can occur. This keeps the verification task computationally feasible and enhances its compositionality. Safety, however, is a more appropriate notion of correctness for concurrent programs than partial correctness. The author shows how the isolation approach to symbolic execution of Ada tasking program supports the verification of general safety properties. Specific safety properties that are considered include mutual exclusion, freedom from deadlock, and absence of communication failure. The techniques are illustrated using a solution to the readers and writers problem.

[1] K. R. Apt, N. Francez, and W. P. de Roever, "A proof system for communicating sequential processes,"ACM Trans. Program Lang. Syst., vol. 2, no. 3, pp. 359-385, July 1980.
[2] G. S. Avrunin, L. K. Dillon, J. C. Wileden, and W. E. Riddle, "Constrained expressions: adding analysis capabilities to design methods for concurrent software systems,"IEEE Trans. Software Eng., vol. SE- 12, pp. 278-292, Feb. 1986.
[3] H. Barringer and I. Mearns, "Axioms and proof rules for Ada tasks," Dep. Comput. Sci., Univ. Manchester, Tech. Rep., 1982: also inProc. IEE, vol. 129, part E, no. 2, 1982.
[4] D. Brand and W. H. Joyner, "Verification of protocols using symbolic execution,"Comput. Networks, vol. 2, pp. 351-360, 1978.
[5] L. K. Dillon, "An isolation approach to symbolic execution-based verification of Ada tasking programs,"J. Syst. Software, to be published.
[6] L. K. Dillon, "Using symbolic execution for verification of Ada tasking programs,"ACM Trans. Program. Lang. Syst., to be published.
[7] L. K. Dillon, R. A. Kremmerer, and L. J. Harrison, "An experience with two symbolic execution-based approaches to formal verification of Ada tasking programs, " inProc. Second Workshop Software Testing, Verification and Analysis. Washington, DC: IEEE Comput. Soc. Press, July 1988, pp. 114-122.
[8] R. W. Floyd, "Assigning meanings to programs," inProc. Amer. Math. Soc. Symp. Applied Mathematics. vol. 19. 1967, pp. 19-31.
[9] R. T. Gerth and W. P. de Roever, "A proof system for concurrent Ada programs," inScience of Computer Programming 4. Amsterdam, The Netherlands: Elsevier, 1984, pp. 159-204.
[10] D. I. Good, R. M. Cohen, and J. Keeton-Williams, "Principles of proving concurrent programs in Gypsy," inProc. 6th Symp. Principles of Programming Languages, ACM, Jan. 1979.
[11] S. L. Hantler and J. C. King, "An introduction to proving the correctness of programs,"ACM Comput. Surveys, vol. 8, no. 3, pp. 331-353, Sept. 1983.
[12] L. J. Harrison and R. A. Kemmerer, "An interleaving symbolic execution approach for the formal verification of Ada programs with tasking," inProc. Third Int. IEEE Conf. Ada Applications and Environments. Washington, DC: IEEE Comput. Soc., May 1988, pp. 15-26.
[13] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[14] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[15] R. A. Kemmerer and S. T. Eckmann, "UNISEX: A UNix-based symbolic Executor for Pascal,"Software-Practice and Experience, vol. 15, no. 5. pp. 439-457, May 1985.
[16] J. C. Knight and V. S. Grine, "Symbolic execution of concurrent Ada programs," Dep. Comput. Sci., Univ. Virginia, Charlottesville, Tech. Rep.
[17] L. Lamport, "The 'Hoare logic' of concurrent programs,"Acta Inform., vol. 14, pp. 21-37, 1980.
[18] L. Lamport and F. B. Schneider, "The 'Hoare logic' of CSP and all that,"ACM Trans. Programming Languages Syst., vol. 6, pp. 281- 296, Apr. 1984.
[19] D. L. Long and L. A. Clarke, "Task interaction graphs for concurrency analysis," Draft, Wellesley College, Wellesley. MA, and Univ. Massachusetts, Amherst, 1988.
[20] D. Mandrioli, R. Zicari, C. Ghezzi, and F. Tisato, "Modeling the Ada task system by Petri nets,"Comput. Lang., vol. 10, no. 1, 1985.
[21] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[22] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE-7. no. 4, pp. 417-426. July 1981.
[23] V. Nguyen, A. Demers, D. Gries, and S. Owicki, "A model and temporal proof system for networks of processes,"Distributed Comput., pp. 7-25, Jan. 1986.
[24] S. Owicki and D. Gries, "Verifying properties of parallel programs: An axiomatic approach,"Commun. ACM, vol. 19, pp. 279-285, May 1976.
[25] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223-252, Sept. 1977.
[26] S. M. Shatz, "Static analysis of Ada programs using the Petri net model," inProc. 1985 Int. Symp. Circuits and Systems, Kyoto, Japan, June 1985, pp. 719-722.
[27] M. Young and R. N. Taylor, "Combining static concurrency analysis with symbolic execution," inProc. Workshop Software Testing, July 1986.

Index Terms:
safety properties verification; Ada tasking programs; isolation approach; symbolic execution; automating partial correctness proofs; concurrent programs; mutual exclusion; deadlock; Ada; multiprocessing programs; program verification.
L.K. Dillon, "Verifying General Safety Properties of Ada Tasking Programs," IEEE Transactions on Software Engineering, vol. 16, no. 1, pp. 51-63, Jan. 1990, doi:10.1109/32.44363
Usage of this product signifies your acceptance of the Terms of Use.