Abstract
As mentioned in the introduction, a formal verification system has several basic elements. First, we require a model. A model is an imaginary universe, or more generally, a class of possible imaginary universes. To make our model meaningful, we require a theory that predicts some or all of the possible observations that might be made of the model. An observation generally takes the form of the truth or falsehood of a predicate, or statement about the model. Finally, to verify something meaningful about the model, we require a methodology for proving statements that are true in the theory.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer Science+Business Media New York
About this chapter
Cite this chapter
McMillan, K.L. (1993). Model Checking. In: Symbolic Model Checking. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-3190-6_2
Download citation
DOI: https://doi.org/10.1007/978-1-4615-3190-6_2
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-6399-6
Online ISBN: 978-1-4615-3190-6
eBook Packages: Springer Book Archive