Specification and verification of concurrent programs by A∀automata

ABSTRACT

∀-automata are non-deterministic finite-state automata over infinite sequences. They differ from conventional automata in that a sequence is accepted if all runs of the automaton over the sequence are accepting. These automata are suggested as a formalism for the specification and verification of temporal properties of concurrent programs. It is shown that they are as expressive as extended-temporal-logic (ETL), and in some cases provide a more compact representation of properties than temporal logic. A structured diagram notation is suggested for the graphical representation of these automata. A single sound and complete proof rule is presented for proving that all computations of a program have the property specified by a ∀-automaton.

REFERENCES

• 1: K. R. Apt , G. D. Plotkin, Countable nondeterminism and random assignment, Journal of the ACM (JACM), v.33 n.4, p.724-767, Oct. 1986 [doi>10.1145/6490.6494]
• 2: B. Alpern, F.B. Schneider -- Verifying Temporal Properties without using Temporal Logic, Technical Report TR 85-723, Cornell University (December 1985).
• 3: 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]
• 4: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 5: E. Allen Emerson , Chin-Laung Lei, Modalities for model checking (extended abstract): branching time strikes back, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318620]
• 6: R.W. Floyd -- Assigning Meanings to Programs, in Mathematical Aspects of Computer Science, 19th Symp. of Appl. Math., American Mathematical Society, Providence (1967), 19-32.
• 7: N. Francez -- Fairness, Springer-Verlag (1986).
• 8: Orna Grumberg , Nissim Francez , Johann A. Makowsky , Willem P. de Roever, A proof rule for fair termination of guarded commands, Information and Control, v.66 n.1-2, p.83-102, July/Aug. 1985 [doi>10.1016/S0019-9958(85)80014-0]
• 9: D. Harel -- Statecharts: A Visual Formalism for Complex Systems, Technical Report, Weizmann Institute (1984).
• 10: David Harel, Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness, Journal of the ACM (JACM), v.33 n.1, p.224-248, Jan. 1986 [doi>10.1145/4904.4993]
• 11: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 12: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 13: Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
• 14: Z. Manna, A. Pnueli -- The Temporal Framework for Concurrent Programming, in The Correctness Problem in Computer Science (R.S. Boyer, J.S. Moore, eds.), Academic Press (1981), 215-274.
• 15: Zohar Manna , Amir Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Science of Computer Programming, v.4 n.3, p.257-289, Dec. 1984 [doi>10.1016/0167-6423(84)90003-0]
• 16: Z. Manna, A. Pnueli -- Specification and Verification of Concurrent Programs by ¿-Automata, Computer Science Report, Stanford University (January 1987).
• 17: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 18: G.L. Peterson -- Myths about the Mutual-exclusion Problem, Information Processing Letters 12, 3 (1981), 115-116.
• 19: F.A. Stomp, W.P. deRoever, R.T. Gerth -- The µ-Calculus as an Assertion Language for Fairness Arguments, Technical Report 84-12, Utrecht (1984).
• 20: M.Y. Vardi, P. Wolper -- An Automata-theoretic Approach to Automatic Program Verification, IEEE Symp. on Logic in Computer Science, Cambridge (1986), 332- 344.
• 21: Pierre Wolper, Temporal logic can be more expressive, Proceedings of the 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981), p.340-348, October 28-30, 1981
• 22: Pierre Wolper , Moshe Y. Vardi , A. Prasad Sistla, Reasoning about infinite computation paths, Proceedings of the 24th Annual Symposium on Foundations of Computer Science (sfcs 1983), p.185-194, November 07-09, 1983 [doi>10.1109/SFCS.1983.51]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification; Specification techniques

General Terms:
Algorithms, Languages, Theory, Verification