Abstract
In a mixed approach to system verification using theorem provers with an interface to specialized model-checking tools, it may be necessary to simplify models by considering abstract versions of them. We report on work in progress that aims to develop support within LAMBDA for a systematic approach to abstraction. We give a formalization in LAMBDA of a notion of abstraction for transition systems; the abstract systems have two sorts of transition, and are related to specifications in modal process logic. We prove that formulae in the modal mu-calculus are satisfied in an abstract version of a model only if they are satisfied in the model itself. We illustrate how the proof of an inductive step in the verification of a satisfaction relation for an infinite model can be reduced to the verification of a satisfaction relation for a very small finite model.
This research was supported by the SERC grant GR/F 31199 ‘Formal System Design Tools’
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J.C. Bradfield. A proof assistant for symbolic model checking. LFCS Report Series ECS-LFCS-92-199, Laboratory for the Foundations of Computer Science, University of Edinburgh, March 1992.
J.C. Bradfield and Colin Stirling. Local model checking for infinite state spaces. Theoretical Computer Science, 96:157–174, 1992.
Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
E.M. Clarke, E. 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, April 1986.
Rance Cleaveland, Joachim Parrow, and Bernhard Steffen. The Concurrency Workbench. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, pages 24–37. Springer-Verlag, 1989. Lecture Notes in Computer Science 407.
E.M.Clarke, O.Grumberg, and D.E.Long. Model checking and abstraction. In Proceedings of the 19th Annual ACM Symposium on Principles of Programming Languages, 1992.
Mick Francis, Simon Finn, Ellie Mayger, and Roger B. Hughes. Reference Manual for the Lambda System. Abstract Hardware Limited, Version 4.2.1 edition, 1992.
Jeffrey J. Joyce and Carl-Johan H. Seger. Linking BDD-based symbolic evaluation to interactive theorem-proving. In Proceedings of the 30th Design Automation Conference. To appear.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.
Kim G. Larsen and Bent Thomsen. A modal process logic. In Proceedings of the Third Annual Symposium on Logic in Computer Science, pages 203–210, 1988.
Monica Nesi. Formalising a modal logic for CCS in the HOL theorem prover. In Luc Claesen and Michael Gordon, editors, Higher Order Logic Theorem Proving and its Applications, Leuven, 1992, pages 279–294. North-Holland, 1993.
Carl-Johan Seger and Jeffrey J. Joyce. A mathematically precise two-level formal verification methodology. Report 92-34, Department of Computer Science, University of British Columbia, December 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McIsaac, A. (1994). A formalization of abstraction in LAMBDA. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_138
Download citation
DOI: https://doi.org/10.1007/3-540-57826-9_138
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57826-0
Online ISBN: 978-3-540-48346-5
eBook Packages: Springer Book Archive