5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 6

They all do so repetitively.Is the value of x always between (and including) 0 and 200? At first sight this seems tobe true. A more thorough inspection, though, reveals that this is not the case. Supposex equals 200. Process Dec tests the value of x, and passes the test, as x exceeds 0.Then, control is taken over by process Reset. It tests the value of x, passes its test, andimmediately resets x to zero. Then, control is returned to process Dec and this processdecrements x by one, resulting in a negative value for x (viz. -1). Intuitively, we tend tointerpret the tests on x and the assignments to x as being executed atomically, i.e., as asingle step, whereas in reality this is (mostly) not the case.Characteristics of Model Checking1.211Characteristics of Model CheckingThis book is devoted to the principles of model checking:Model checking is an automated technique that, givena finite-state model of a system and a formal property,systematically checks whether this property holdsfor (a given state in) that model.The next chapters treat the elementary technical details of model checking.

This sectiondescribes the process of model checking (how to use it), presents its main advantages anddrawbacks, and discusses its role in the system development cycle.1.2.1The Model-Checking ProcessIn applying model checking to a design the following different phases can be distinguished:• Modeling phase:– model the system under consideration using the model description language ofthe model checker at hand;– as a first sanity check and quick assessment of the model perform some simulations;– formalize the property to be checked using the property specification language.• Running phase: run the model checker to check the validity of the property in thesystem model.• Analysis phase:– property satisfied? → check next property (if any);– property violated? →1.

analyze generated counterexample by simulation;2. refine the model, design, or property;3. repeat the entire procedure.– out of memory? → try to reduce the model and try again.12System VerificationIn addition to these steps, the entire verification should be planned, administered, andorganized. This is called verification organization. We discuss these phases of modelchecking in somewhat more detail below.Modeling The prerequisite inputs to model checking are a model of the system underconsideration and a formal characterization of the property to be checked.Models of systems describe the behavior of systems in an accurate and unambiguousway. They are mostly expressed using finite-state automata, consisting of a finite setof states and a set of transitions. States comprise information about the current valuesof variables, the previously executed statement (e.g., a program counter), and the like.Transitions describe how the system evolves from one state into another.

For realisticsystems, finite-state automata are described using a model description language such asan appropriate dialect/extension of C, Java, VHDL, or the like. Modeling systems, inparticular concurrent ones, at the right abstraction level is rather intricate and is reallyan art; it is treated in more detail in Chapter 2.In order to improve the quality of the model, a simulation prior to the model checkingcan take place.

Simulation can be used effectively to get rid of the simpler category ofmodeling errors. Eliminating these simpler errors before any form of thorough checkingtakes place may reduce the costly and time-consuming verification effort.To make a rigorous verification possible, properties should be described in a precise andunambiguous manner. This is typically done using a property specification language. Wefocus in particular on the use of a temporal logic as a property specification language,a form of modal logic that is appropriate to specify relevant properties of ICT systems.In terms of mathematical logic, one checks that the system description is a model ofa temporal logic formula.

This explains the term “model checking”. Temporal logic isbasically an extension of traditional propositional logic with operators that refer to thebehavior of systems over time. It allows for the specification of a broad range of relevantsystem properties such as functional correctness (does the system do what it is supposedto do?), reachability (is it possible to end up in a deadlock state?), safety (“somethingbad never happens”), liveness (“something good will eventually happen”), fairness (does,under certain conditions, an event occur repeatedly?), and real-time properties (is thesystem acting in time?).Although the aforementioned steps are often well understood, in practice it may be aserious problem to judge whether the formalized problem statement (model + properties)is an adequate description of the actual verification problem.

This is also known as thevalidation problem. The complexity of the involved system, as well as the lack of precisionCharacteristics of Model Checking13of the informal specification of the system’s functionality, may make it hard to answer thisquestion satisfactorily. Verification and validation should not be confused.

Verificationamounts to check that the design satisfies the requirements that have been identified, i.e.,verification is “check that we are building the thing right”. In validation, it is checkedwhether the formal model is consistent with the informal conception of the design, i.e.,validation is “check that we are verifying the right thing”.Running the Model Checker The model checker first has to be initialized by appropriately setting the various options and directives that may be used to carry out theexhaustive verification.

Subsequently, the actual model checking takes place. This isbasically a solely algorithmic approach in which the validity of the property under consideration is checked in all states of the system model.Analyzing the Results There are basically three possible outcomes: the specifiedproperty is either valid in the given model or not, or the model turns out to be too largeto fit within the physical limits of the computer memory.In case the property is valid, the following property can be checked, or, in case all propertieshave been checked, the model is concluded to possess all desired properties.Whenever a property is falsified, the negative result may have different causes. There maybe a modeling error, i.e., upon studying the error it is discovered that the model does notreflect the design of the system. This implies a correction of the model, and verificationhas to be restarted with the improved model. This reverification includes the verificationof those properties that were checked before on the erroneous model and whose verificationmay be invalidated by the model correction! If the error analysis shows that there is noundue discrepancy between the design and its model, then either a design error has beenexposed, or a property error has taken place.

In case of a design error, the verificationis concluded with a negative result, and the design (together with its model) has to beimproved. It may be the case that upon studying the exposed error it is discovered that theproperty does not reflect the informal requirement that had to be validated. This impliesa modification of the property, and a new verification of the model has to be carried out.As the model is not changed, no reverification of properties that were checked before hasto take place.

The design is verified if and only if all properties have been checked withrespect to a valid model.Whenever the model is too large to be handled – state spaces of real-life systems may bemany orders of magnitude larger than what can be stored by currently available memories– there are various ways to proceed. A possibility is to apply techniques that try to exploit14System Verificationimplicit regularities in the structure of the model. Examples of these techniques are therepresentation of state spaces using symbolic techniques such as binary decision diagramsor partial order reduction. Alternatively, rigorous abstractions of the complete systemmodel are used.

These abstractions should preserve the (non-)validity of the propertiesthat need to be checked. Often, abstractions can be obtained that are sufficiently smallwith respect to a single property. In that case, different abstractions need to be made forthe model at hand. Another way of dealing with state spaces that are too large is to giveup the precision of the verification result. The probabilistic verification approaches exploreonly part of the state space while making a (often negligible) sacrifice in the verificationcoverage.

The most important state-space reduction strategies are discussed in Chapters7 through 9 of this monograph.Verification Organization The entire model-checking process should be well organized, well structured, and well planned. Industrial applications of model checking haveprovided evidence that the use of version and configuration management is of particularrelevance. During the verification process, for instance, different model descriptions aremade describing different parts of the system, various versions of the verification models are available (e.g., due to abstraction), and plenty of verification parameters (e.g.,model-checking options) and results (diagnostic traces, statistics) are available.

This information needs to be documented and maintained very carefully in order to manage apractical model-checking process and to allow the reproduction of the experiments thatwere carried out.1.2.2Strengths and WeaknessesThe strengths of model checking:• It is a general verification approach that is applicable to a wide range of applicationssuch as embedded systems, software engineering, and hardware design.• It supports partial verification, i.e., properties can be checked individually, thusallowing focus on the essential properties first.