Abstract
We present an overview of SMG, a generic state machine generator, which interfaces to various temporal logic model checkers and provides a practical generic temporal verification system. SMG transforms programs written in user-definable languages to suitable finite state models. thus enabling fast verification of temporal properties of the input program. It can be applied, in particular, to the verification of temporal properties of concurrent and reactive systems.
Research supported under Alvey/SERC grant GR/D/57492
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
H. Barringer. Using Temporal Logic in the Compositional Specification of Concurrent Systems. In A. P. Galton, editor, Temporal Logics and their Applications, chapter 2, pages 53–90, Academic Press Inc. Limited, London, December 1987.
M.C. Browne and E.M. Clarke. SML — a high level language for the design and verification of finite state machines. In From H.D.L. descriptions to guaranteed correct circuit designs, IFIP, September 1986.
M.C. Browne, E.M. Clarke, D. Dill, and B. Mishra. Automatic Verification of Sequential Circuits using Temporal Logic. Technical Report CS-85-100, Department of Computer Science, Carnegie-Mellon University, 1984.
H. Barringer and G.D. Gough. Mechanisation of Temporal Logics. Part 1: Techniques. Temple internal report, Department of Computer Science, University of Manchester, 1987.
H. Barringer, R. Kuiper, and A. Pnueli. Now You May Compose Temporal Logic Specifications. In Proceedings of the Sixteenth ACM Symposium on the Theory of Computing, 1984.
H. Barringer, R. Kuiper, and A. Pnueli. A Really Abstract Concurrent Model and its Temporal Logic. In Proceedings of the Thirteenth ACM Symposium on the Principles of Programming Languages, St. Petersberg Beach, Florida, January 1986.
M.C. Browne. An improved algorithm for the automatic verification of finite state systems using temporal logic. Technical Report, Department of Computer Science, Carnegie-Mellon University, December 1986.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
E. M. Clarke, O. Grümberg, and M. C. Browne. Reasoning about networks with many identical finite-state processes. In Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, ACM, August 1986.
G. D. Gough. Decision Procedures for Temporal Logic. Master's thesis, Department of Computer Science, University of Manchester, October 1984.
Stephen C. Johnson. Yacc: Yet another compiler-compiler. Unix Programmer's Manual Vol 2b, 1979.
L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, July 1983.
L. Lamport. What good is temporal logic. In R. E. A. Mason, editor, Information Processing 83, pages 657–668, IFIP, Elsevier Science Publishers B.V. (North-Holland), 1983.
L. Lamport. An Axiomatic Semantics of Concurrent Programming Languages. In Krysztof Apt, editor, Logics and Models of Concurrent Systems, pages 77–122, NATO, Springer-Verlag, La Colle-sur-Loup, France, October 1984.
Z. Manna and A. Pnueli. Verification of Concurrent Programs: The Temporal Framework. In Robert S. Boyer and J. Strother Moore, editors, The Correctness Problem in Computer Science, Academic Press, London, 1982.
S. Owicki and L. Lamport. Proving Liveness Properties of Concurrent Programs. ACM Transactions on Programming Languages and Systems, 4(3):455–495, July 1982.
G. L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115–116, 1981.
G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Department of Computer Science,Aarhus University, September 1981.
A. Pnueli. The Temporal Logic of Programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science, Providence, November 1977.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In Krysztof Apt, editor, Logics and Models of Concurrent Systems, pages 123–144, NATO, Springer-Verlag, La Colle-sur-Loup, France, October 1984.
J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. Lecture Notes in Computer Science, 137, April 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gough, G.D., Barringer, H. (1988). A semantics driven temporal verification system. In: Ganzinger, H. (eds) ESOP '88. ESOP 1988. Lecture Notes in Computer Science, vol 300. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19027-9_2
Download citation
DOI: https://doi.org/10.1007/3-540-19027-9_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19027-1
Online ISBN: 978-3-540-38941-5
eBook Packages: Springer Book Archive