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

It is not surprisingthat chip manufacturers invest a lot in getting their designs right. Hardware verificationis a well-established part of the design process. The design effort in a typical hardwaredesign amounts to only 27% of the total time spent on the chip; the rest is devoted toerror detection and prevention.Hardware verification techniques. Emulation, simulation, and structural analysis are themajor techniques used in hardware verification.Structural analysis comprises several specific techniques such as synthesis, timing analysis,and equivalence checking that are not described in further detail here.Emulation is a kind of testing.

A reconfigurable generic hardware system (the emulator) isconfigured such that it behaves like the circuit under consideration and is then extensivelytested. As with software testing, emulation amounts to providing a set of stimuli to thecircuit and comparing the generated output with the expected output as laid down inthe chip specification.

To fully test the circuit, all possible input combinations in everypossible system state should be examined. This is impractical and the number of testsneeds to be reduced significantly, yielding potential undiscovered errors.With simulation, a model of the circuit at hand is constructed and simulated. Models aretypically provided using hardware description languages such as Verilog or VHDL thatare both standardized by IEEE. Based on stimuli, execution paths of the chip model areexamined using a simulator.

These stimuli may be provided by a user, or by automatedmeans such as a random generator. A mismatch between the simulator’s output and theoutput described in the specification determines the presence of errors. Simulation is liketesting, but is applied to models. It suffers from the same limitations, though: the numberof scenarios to be checked in a model to get full confidence goes beyond any reasonablesubset of scenarios that can be examined in practice.Simulation is the most popular hardware verification technique and is used in variousdesign stages, e.g., at register-transfer level, gate and transistor level. Besides these errordetection techniques, hardware testing is needed to find fabrication faults resulting fromlayout defects in the fabrication process.Model Checking1.17Model CheckingIn software and hardware design of complex systems, more time and effort are spent onverification than on construction.

Techniques are sought to reduce and ease the verificationefforts while increasing their coverage. Formal methods offer a large potential to obtain anearly integration of verification in the design process, to provide more effective verificationtechniques, and to reduce the verification time.Let us first briefly discuss the role of formal methods. To put it in a nutshell, formalmethods can be considered as “the applied mathematics for modeling and analyzing ICTsystems”. Their aim is to establish system correctness with mathematical rigor. Theirgreat potential has led to an increasing use by engineers of formal methods for the verification of complex software and hardware systems. Besides, formal methods are oneof the “highly recommended” verification techniques for software development of safetycritical systems according to, e.g., the best practices standard of the IEC (InternationalElectrotechnical Commission) and standards of the ESA (European Space Agency).

Theresulting report of an investigation by the FAA (Federal Aviation Authority) and NASA(National Aeronautics and Space Administration) about the use of formal methods concludes thatFormal methods should be part of the education of every computer scientistand software engineer, just as the appropriate branch of applied maths is anecessary part of the education of all other engineers.During the last two decades, research in formal methods has led to the development ofsome very promising verification techniques that facilitate the early detection of defects.These techniques are accompanied by powerful software tools that can be used to automatevarious verification steps. Investigations have shown that formal verification procedureswould have revealed the exposed defects in, e.g., the Ariane-5 missile, Mars Pathfinder,Intel’s Pentium II processor, and the Therac-25 therapy radiation machine.Model-based verification techniques are based on models describing the possible systembehavior in a mathematically precise and unambiguous manner.

It turns out that – priorto any form of verification – the accurate modeling of systems often leads to the discovery of incompleteness, ambiguities, and inconsistencies in informal system specifications.Such problems are usually only discovered at a much later stage of the design. The systemmodels are accompanied by algorithms that systematically explore all states of the systemmodel.

This provides the basis for a whole range of verification techniques ranging from anexhaustive exploration (model checking) to experiments with a restrictive set of scenariosin the model (simulation), or in reality (testing). Due to unremitting improvements of un-8System Verificationderlying algorithms and data structures, together with the availability of faster computersand larger computer memories, model-based techniques that a decade ago only worked forvery simple examples are nowadays applicable to realistic designs.

As the startingpointof these techniques is a model of the system under consideration, we have as a given factthatAny verification using model-based techniques is onlyas good as the model of the system.Model checking is a verification technique that explores all possible system states in abrute-force manner. Similar to a computer chess program that checks possible moves, amodel checker, the software tool that performs the model checking, examines all possiblesystem scenarios in a systematic manner. In this way, it can be shown that a given systemmodel truly satisfies a certain property. It is a real challenge to examine the largest possiblestate spaces that can be treated with current means, i.e., processors and memories. Stateof-the-art model checkers can handle state spaces of about 108 to 109 states with explicitstate-space enumeration.

Using clever algorithms and tailored data structures, larger statespaces (1020 up to even 10476 states) can be handled for specific problems. Even the subtleerrors that remain undiscovered using emulation, testing and simulation can potentiallybe revealed using model checking.requirementssystemFormalizingModelingpropertyspecificationsystem modelModel Checkingsatisfiedviolated +counterexampleSimulationlocationerrorFigure 1.4: Schematic view of the model-checking approach.Typical properties that can be checked using model checking are of a qualitative nature:Is the generated result OK?, Can the system reach a deadlock situation, e.g., when twoModel Checking9concurrent programs are waiting for each other and thus halting the entire system? Butalso timing properties can be checked: Can a deadlock occur within 1 hour after a systemreset?, or, Is a response always received within 8 minutes? Model checking requires aprecise and unambiguous statement of the properties to be examined.

As with makingan accurate system model, this step often leads to the discovery of several ambiguitiesand inconsistencies in the informal documentation. For instance, the formalization of allsystem properties for a subset of the ISDN user part protocol revealed that 55% (!) of theoriginal, informal system requirements were inconsistent.The system model is usually automatically generated from a model description that isspecified in some appropriate dialect of programming languages like C or Java or hardware description languages such as Verilog or VHDL. Note that the property specificationprescribes what the system should do, and what it should not do, whereas the modeldescription addresses how the system behaves. The model checker examines all relevantsystem states to check whether they satisfy the desired property. If a state is encounteredthat violates the property under consideration, the model checker provides a counterexample that indicates how the model could reach the undesired state.

The counterexampledescribes an execution path that leads from the initial system state to a state that violatesthe property being verified. With the help of a simulator, the user can replay the violatingscenario, in this way obtaining useful debugging information, and adapt the model (or theproperty) accordingly (see Figure 1.4).Model checking has been successfully applied to several ICT systems and their applications.For instance, deadlocks have been detected in online airline reservation systems, modern ecommerce protocols have been verified, and several studies of international IEEE standardsfor in-house communication of domestic appliances have led to significant improvementsof the system specifications.

Five previously undiscovered errors were identified in anexecution module of the Deep Space 1 spacecraft controller (see Figure 1.5), in one caseidentifying a major design flaw. A bug identical to one discovered by model checkingescaped testing and caused a deadlock during a flight experiment 96 million km fromearth. In the Netherlands, model checking has revealed several serious design flaws in thecontrol software of a storm surge barrier that protects the main port of Rotterdam againstflooding.Example 1.1.Concurrency and AtomicityMost errors, such as the ones exposed in the Deep Space-1 spacecraft, are concernedwith classical concurrency errors. Unforeseen interleavings between processes may causeundesired events to happen.

This is exemplified by analysing the following concurrentprogram, in which three processes, Inc, Dec, and Reset, cooperate. They operate on theshared integer variable x with arbitrary initial value that can be accessed (i.e., read), and10System VerificationFigure 1.5: Modules of NASA’s Deep Space-1 space-craft (launched in October 1998) havebeen thoroughly examined using model checking.modified (i.e., written) by each of the individual processes. The processes areproc Inc = while true do if x < 200 then x := x + 1 fi odproc Dec = while true do if x > 0 then x := x − 1 fi odproc Reset = while true do if x = 200 then x := 0 fi odProcess Inc increments x if its value is smaller than 200, Dec decrements x if its value is atleast 1, and Reset resets x once it has reached the value 200.