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

No complete requirement specificationis needed.• It is not vulnerable to the likelihood that an error is exposed; this contrasts withtesting and simulation that are aimed at tracing the most probable defects.• It provides diagnostic information in case a property is invalidated; this is very usefulfor debugging purposes.Characteristics of Model Checking15• It is a potential “push-button” technology; the use of model checking requires neithera high degree of user interaction nor a high degree of expertise.• It enjoys a rapidly increasing interest by industry; several hardware companies havestarted their in-house verification labs, job offers with required skills in model checking frequently appear, and commercial model checkers have become available.• It can be easily integrated in existing development cycles; its learning curve is notvery steep, and empirical studies indicate that it may lead to shorter developmenttimes.• It has a sound and mathematical underpinning; it is based on theory of graph algorithms, data structures, and logic.The weaknesses of model checking:• It is mainly appropriate to control-intensive applications and less suited for dataintensive applications as data typically ranges over infinite domains.• Its applicability is subject to decidability issues; for infinite-state systems, or reasoning about abstract data types (which requires undecidable or semi-decidable logics),model checking is in general not effectively computable.• It verifies a system model, and not the actual system (product or prototype) itself;any obtained result is thus as good as the system model.

Complementary techniques,such as testing, are needed to find fabrication faults (for hardware) or coding errors(for software).• It checks only stated requirements, i.e., there is no guarantee of completeness. Thevalidity of properties that are not checked cannot be judged.• It suffers from the state-space explosion problem, i.e., the number of states neededto model the system accurately may easily exceed the amount of available computermemory.

Despite the development of several very effective methods to combat thisproblem (see Chapters 7 and 8), models of realistic systems may still be too large tofit in memory.• Its usage requires some expertise in finding appropriate abstractions to obtain smallersystem models and to state properties in the logical formalism used.• It is not guaranteed to yield correct results: as with any tool, a model checker maycontain software defects.22Parts of the more advanced model-checking procedures have been formally proven correct using theorem provers to circumvent this.16System Verification• It does not allow checking generalizations: in general, checking systems with an arbitrary number of components, or parameterized systems, cannot be treated.

Modelchecking can, however, suggest results for arbitrary parameters that may be verifiedusing proof assistants.We believe that one can never achieve absolute guaranteed correctness for systems ofrealistic size. Despite the above limitations we conclude thatModel checking is an effective techniqueto expose potential design errors.Thus, model checking can provide a significant increase in the level of confidence of asystem design.1.3Bibliographic NotesModel checking. Model checking originates from the independent work of two pairs inthe early eighties: Clarke and Emerson [86] and Queille and Sifakis [347]. The termmodel checking was coined by Clarke and Emerson. The brute-force examination of theentire state space in model checking can be considered as an extension of automatedprotocol validation techniques by Hajek [182] and West [419, 420].

While these earliertechniques were restricted to checking the absence of deadlocks or livelocks, model checkingallows for the examination of broader classes of properties. Introductory papers on modelchecking can be found in [94, 95, 96, 293, 426]. The limitations of model checking werediscussed by Apt and Kozen [17]. More information on model checking is available in theearlier books by Holzmann [205], McMillan [288], and Kurshan [250] and the more recentworks by Clarke, Grumberg, and Peled [92], Huth and Ryan [219], Schneider [365], andBérard et al. [44].

The model-checking trajectory has recently been described by Ruysand Brinksma [360].Software verification. Empirical data about software engineering is gathered by the Center for Empirically Based Software Engineering (www.cebase.org); their collected dataabout software defects has recently been summarized by Boehm and Basili [53]. The different characterizations of verification (“are we building the thing right?”) and validation(“are we building the right thing?”) originate from Boehm [52]. An overview of softwaretesting is given by Whittaker [421]; books about software testing are by Myers [308] andBeizer [36].

Testing based on formal specifications has been studied extensively in the areaof communication protocols. This has led to an international standard for conformanceBibliographic Notes17testing [222]. The use of software verification techniques by the German software industryhas been studied by Liggesmeyer et al. [275]. Books by Storey [381] and Leveson [269]describe techniques for developing safety-critical software and discuss the role of formalverification in this context. Rushby [359] addresses the role of formal methods for developing safety-critical software. The book of Peled [327] gives a detailed account of formaltechniques for software reliability that includes testing, model checking, and deductivemethods.Model-checking software.

Model-checking communication protocols has become popularthrough the pioneering work of Holzmann [205, 206]. An interesting project at Bell Labsin which a model-checking team and a traditional design team worked on the design ofpart of the ISDN user part protocol has been reported by Holzmann [207]. In this largecase study, 112 serious design flaws were discovered while checking 145 formal properties inabout 10,000 verification runs.

Errors found by Clarke et al. [89] in the IEEE Futurebus+standard (checking a model of more than 1030 states) has led to a substantial revision ofthe protocol by IEEE. Chan et al. [79] used model checking to verify the control softwareof a traffic control and alert system for airplanes. Recently, Staunstrup et al. [377] havereported the succesful model checking of a train model consisting of 1421 state machinescomprising a state space of 10476 states. Lowe [278], using model checking, discovered aflaw in the well-known Needham-Schroeder authentication algorithm that remained undetected for over 17 years.

The usage of formal methods (that includes model checking)in the software development process of a safety-critical system within a Dutch softwarehouse is presented by Tretmans, Wijbrans, and Chaudron [393]. The formal analysis ofNASA’s Mars Pathfinder and the Deep Space-1 spacecraft are addressed by Havelund,Lowry, and Penix [194], and Holzmann, Najm, and Serhrouchini [210], respectively. Theautomated generation of abstract models amenable to model checking from programswritten in programming languages such as C, C++, or Java has been pursued, for instance,by Godefroid [170], Dwyer, Hatcliff, and coworkers [193], at Microsoft Research by Ball,Podelski, and Rajamani [33] and at NASA Research by Havelund and Pressburger [195].Model-checking hardware.

Applying model checking to hardware originates from Browneet al. [66] analyzing some moderate-size self-timed sequential circuits. Successful applications of (symbolic) model checking to large hardware systems have been first reportedby Burch et al. [75] in the early nineties. They analyzed a synchronous pipeline circuitof approximately 1020 states. Overviews of formal hardware verification techniques canbe found in works by Gupta [179], and the books by Yoeli [428] and Kropf [246]. Theneed for formal verification techniques for hardware verification has been advocated by,among others, Sangiovanni-Vincentelli, McGeer, and Saldanha [362].

The integration ofmodel-checking techniques for error finding in the hardware development process at IBMhas been recently described by Schlipf et al. [364] and Abarbanel-Vinov et al. [2]. Theyconclude that model checking is a powerful extension of the traditional verification pro-18System Verificationcess, and consider it as complementary to simulation/emulation. The design of a memorybus adapter at IBM showed, e.g., that 24% of all defects were found with model checking,while 40% of these errors would most likely not have been found by simulation.Chapter 2Modelling Concurrent SystemsA prerequisite for model checking is a model of the system under consideration.

Thischapter introduces transition systems, a (by now) standard class of models to representhardware and software systems. Different aspects for modeling concurrent systems aretreated, ranging from the simple case in which processes run completely autonomouslyto the more realistic setting where processes communicate in some way. The chapter isconcluded by considering the problem of state-space explosion.2.1Transition SystemsTransition systems are often used in computer science as models to describe the behavior ofsystems. They are basically directed graphs where nodes represent states, and edges modeltransitions, i.e., state changes.