Techniques for temporal logic model checking

Model checking is a set of formal verification techniques that aim to show that a structure representing a computational system (for instance, a protocol, or a hardware or a software component, among others) is a model for a property that represents a requirement for this system. Many model-checking approaches have been proposed, depending on the formalism the property is expressed in, and the class of structures used to represent the system under verification. In the next section, we motivate the use of model-checking, and summarize the research work that has been carried out in this area. In Section 2, we discuss Kripke structures, one of the main state-transition models in the model-checking literature. Section 3 is devoted to propositional temporal logics commonly used in the realm of program verification: CTL*, CTL and LTL. Their expressiveness is compared and illustrated. Section 4 provides the key components of explicit model-checking for the temporal logic LTL, and introduces some advanced techniques that are used in current implementations such as the SPIN model-checker. Then, in Section 5, we present the decision procedure for CTL as originally proposed in the seminal work of [62] and [218]. Next, in Section 6, we present how Kripke structures can be represented and analyzed using quantified propositional logic, and introduce Binary Decision Diagrams (BDDs), an efficient implementation of this logic; at that point we are ready to present symbolic model-checking. We also present the symbolic model-checking features of the NuSMV model-checker. Section 7 is devoted to so-called bounded model-checking. This technique makes it possible to verify (in general partially) LTL properties of much larger structures than the previous approaches. We also present the bounded model-checking features of NuSMV. Finally, in Section 8, we briefly touch upon some of the most recent developments in formal verification of software, some of which employ techniques that had been initially developed to enhance model checkers.