Abstract
SMG [GB88] is a system designed to generate a finite state model of a program from the program itself and an operational semantics for the programming language. Model-checking can then be used to verify that the program satisfies a set of desired temporal properties.
In this paper we first show how we have incorporated notions of fairness into SMG; in particular, a user is now able to define semantics with “fair” constructs, for example, parallel composition, repetitive choice, etc. A program may contain several fair constructs, each with its own fairness type. Secondly we describe a practical approach to model checking of linear temporal formulae over the fair-satisfiability generated by the new SMGF. Our approach is a refinement and extension of the fair-satisfiability algorithms, presented earlier by Lichtenstein and Pnueli [LP85], together with techniques developed in our practical implementations of decision procedures for linear temporal logic [Gou84].
This research has been performed as part of the TEMPLE project and is fully supported under Alvey PRJ/SE/054 (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
Michael 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.
Constantin Courcoubetis, Moshe Y. Vardi, and Pierre Wolper. Reasoning About Fair Concurrent Programs. Technical Report RJ 5149 (53489), IBM Almaden Research Center, San Jose, California, May 1986.
Michael D. Fisher. A Model Checker for Linear Time Temporal Logic. Temple project report, Department of Computer Science, University of Manchester, February 1989.
G. D. Gough and H. Barringer. A Semantics Driven Temporal Verification System. In Proceedings of ESOP '88, March 1988.
G. D. Gough and H. Barringer. Mechanisation of Temporal Logics. Part 2: Practical Decision Procedures. Temple project report, Department of Computer Science, University of Manchester, 1989. (forthcoming).
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.
O. Lichtenstein and A. Pnueli. Checking that Finite State Concurrent Programs Satisfy their Linear Specification. In Proceedings of the Twelfth ACM Symposium on the Principles of Programming Languages, New Orleans, Louisiana, January 1985.
D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. Lecture Notes in Computer Science, 115, July 1981.
G. D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, September 1981.
J.L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Xesar User's Manual. Technical report, Laboratoire de Genie Informatique, IMAG, Grenoble, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barringer, H., Fisher, M.D., Gough, G.D. (1990). Fair SMG and linear time model checking. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_12
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive