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.
KeywordsModel Check Temporal Logic Linear Temporal Logic Atomic Proposition Kripke Model
Unable to display preview. Download preview PDF.