Abstract
A new method for analyzing specifications in languages like Z and VDM is proposed. Theorems are checked automatically by exhaustive search of the state space. An abstraction over the actual states can be defined that reduces an infinite state space to a finite number of equivalence classes, allowing it to be searched exhaustively by treating each class as a single abstract state. A prototype has been built that has verified some small theorems from the literature.
This research was sponsored in part by a Research Initiation Award from the National Science Foundation (NSF), under grant CCR-9308726, by a grant from the TRW Corporation, and by the Wright Laboratory, Aeronautical Systems Center, Air Force Materiel Command, USAF, and the Advanced Research Projects Agency (ARPA), under grant F33615-93-1-1330. The text faces were generously provided by Bitstream, Inc.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. Ackermann, Solvable Cases of the Decision Problem, North-Holland Publishing Company, Amsterdam, 1954.
J.M. Atlee and J.D. Cannon, “State-based Model Checking of Event-Driven Systems Requirements”, IEEE Transactions on Software Engineering, Jan. 1993.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and J. Hwang, “Symbolic Model Checking: 1020 States and Beyond”, Information and Computation, 98(2), pp. 105–120, 1992.
L. Bachmair, H. Gandzinger and U. Waldmann, Set Constraints are the Monadic Class, Technical Report MPI-I-92-240, Max Planck Institute for Computer Science, December 1992.
Francois Bourdoncle, “Abstract Debugging of Higher-Order Imperative Languages”, Proc. ACM Symposium of Programming Language Design and Implementation, June 1993.
R.E. Bryant, “Verifying a Static RAM Design by Logic Simulation”, pp. 335–349 of Advanced Research in VLSI: Proceedings of the Fifth MIT Conference, ed. J. Allen and F.T. Leighton, MIT Press, 1988.
P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”, Proc. 4th ACM Symposium on Principle of Programming Languages, pp. 238–252, January 1977.
E.M. Clarke, E.A. Emerson and A.P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications”, ACM Transactions of Programming Languages and Systems, 8(2), pp. 244–263, 1986.
E.M. Clarke, O. Grumberg and D.E. Long, “Model Checking and Abstraction”, Proc. ACM Symposium of Principles of Programming Languages, January 1992.
R. Cleaveland, J. Parrow and B. Steffen, “The Concurrency Workbench”, Proc. of the Workshop on Automatic Verification Methods for Finite-State Systems, pp. 24–37, Lecture Notes in Computer Science 407, Springer-Verlag, Berlin, 1989.
John V Guttag and James J. Horning, “Formal Specification as a Design Tool”, Seventh ACM Symp. on Principles of Programming Languages, Las Vegas, January 1980.
John Guttag, James Horning and Jeannette Wing, “The Larch Family of Specification Languages”, IEEE Software, Sept. 1985.
A. Ferro, E.G. Omodeo and J.T. Schwanz, “Decision Procedures for Elementary Sublanguages of Set Theory. I. Multi-level Syllogistic and Some Extensions”. Communications on Pure and Applied Mathematics, 40, pp. 265–280, 1987.
FDR: User Manual and Tutorial, Formal Systems Europe Ltd., Oxford, England, October 1992.
David Harel, “Statecharts: A Visual Formalism for Complex Systems”, Science of Computer Programming, 8, pp. 231–274, 1987.
Ian Hayes, ed., Specification Case Studies, Prentice Hall International, 2nd ed., 1993.
Peter Henderson, “Finite State Modelling in Program Development”, Proc. International Conference on Reliable Software, Los Angeles, 1975.
N. Heintze and J. Jaffar, “A Decision Procedure for a Class of Herbrand Set Constraints”, Proc. 5th IEEE Symposium on Logic in Computer Science, June 1990.
Cliff B. Jones, Systematic Software Development Using VDM, Prentice Hall International, 1986.
R.P. Kurshan, Testing Containment of ω-Regular Languages, Technical Report 1121-861010-33-TM, AT&T Bell Laboratories, 1986.
Greg Nelson and Derek C. Oppen, “Fast Decision Procedures Based on Congruence Closure”, Journal of the Association for Computing Machinery, 27(2), April 1980.
D. Parnas and J. Madey, Functional Documentation for Computer Systems Engineering, Technical Report TR-90-287, Queen's University, Kingston, Ontario, September 1990.
Ben Potter, Jane Sinclair and David Till, An Introduction to Formal Specification in Z, Prentice-Hall International, 1991.
J.M. Spivey, The Z Notation: A Reference Manual, Prentice Hall International, 1989.
Robert E. Strom, “Mechanisms for Compile-time Enforcement of Security”, Proc. ACM Symposium of Principles of Programming Languages, January 1983.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jackson, D. (1994). Abstract model checking of infinite specifications. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_113
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_113
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive