Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach

ABSTRACT

We give an efficient procedure for verifying that a finite state concurrent system meets a specification expressed in a (propositional) branching-time temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global transition graph for the concurrent system. We also show how the logic and our algorithm can be modified to handle fairness. We argue that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.

REFERENCES

• 1: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 2: K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
• 3: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 4: E. Allen Emerson , Edmund M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.169-181, July 14-18, 1980
• 5: E. Allen Emerson , Joseph Y. Halpern, "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report), Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.127-140, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567081]
• 6: Brent T. Hailpern , Susan S. Owicki, Verifying network protocols using temporal logic, Stanford University, Stanford, CA, 1980
• 7: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 8: Z. Manna, A. Pneuli. "Verification of Concurrent Programs: The Temporal Framework." The Correctness Problem in Computer Science (R. S. Boyer and J. S. Moore, eds.), International Lecture Series in Computer Science (1981).
• 9: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, Logic of Programs, Workshop, p.253-281, May 01, 1981
• 10: S. Owicki, L. Lamport. "Proving Liveness Properties of Concurrent Programs." Stanford University Technical Report (1980).
• 11: J. P. Quielle, J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. Proceedings of the Fifth International Symposium in Programming, 1981.
• 12: J. P. Quielle, J. Sifakis. "Fairness and Related Properties in Transition Systems." IMAG, 292 (March 1982).
• 13: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.159-168, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802189]
• 14: Deepinder P. Sidhu, Rules for synthesizing correct communication protocols, ACM SIGCOMM Computer Communication Review, v.12 n.1, p.35-51, January 1982 [doi>10.1145/1040119.1040122]
• 15: P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand. "Towards Analyzing and Synthesizing Protocols." IEEE Transactions on Communications COM-28, 4 (April 1980), 651-671.