Abstract
This chapter provides a brief introduction to the domain of formal methods (Boca, Bowen, & Siddiqi, 2009) and the most commonly used verification methods (i.e., theorem proving [Harrison, 2009] and model checking [Baier & Katoen, 2008]). Due to their inherent precision, formal verification methods are increasingly being used in modeling and verifying safety and financial-critical systems these days.
Top2.2 Model Checking
Model checking is primary used as the verification technique for reactive systems, i.e., the systems whose behavior is dependent on time and their environment, like controller units of digital circuits and communication protocols. The inputs to a model checker include the finite-state model of the system that needs to be analyzed along with the intended system properties, which are expressed in temporal logic. The model checker automatically verifies if the properties hold for the given system while providing an error trace in case of a failing property. The main verification principle behind model-checking is to construct a precise state-based model of the given system and exhaustively verify the given property for each state of this model. The analysis is automatic which is why model checking is one of the most widely used formal verification technique. On the other hand, model-checking is limited to systems that can only be expressed as finite-state machines. Another major limitation of the model checking approach is state space explosion. The state-space of a system can be very large, or sometimes even infinite. Thus, it becomes computationally impossible to explore the entire state-space with limited resources of time and memory. This problem is usually resolved by working with abstract, less complex, models of the system by somewhat compromising the accuracy of the analysis.