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

The fatal defects in the controlsoftware of the Ariane-5 missile (Figure 1.1), the Mars Pathfinder, and the airplanes ofthe Airbus family led to headlines in newspapers all over the world and are notorious bynow. Similar software is used for the process control of safety-critical systems such aschemical plants, nuclear power plants, traffic control and alert systems, and storm surgebarriers. Clearly, bugs in such software can have disastrous consequences. For example, asoftware flaw in the control part of the radiation therapy machine Therac-25 caused thedeath of six cancer patients between 1985 and 1987 as they were exposed to an overdoseof radiation.The increasing reliance of critical applications on information processing leads us to state:The reliability of ICT systems is a key issuein the system design process.The magnitude of ICT systems, as well as their complexity, grows apace.

ICT systemsare no longer standalone, but are typically embedded in a larger context, connectingand interacting with several other components and systems. They thus become muchmore vulnerable to errors – the number of defects grows exponentially with the numberof interacting system components. In particular, phenomena such as concurrency andnondeterminism that are central to modeling interacting systems turn out to be very hardto handle with standard techniques. Their growing complexity, together with the pressureto drastically reduce system development time (“time-to-market”), makes the delivery oflow-defect ICT systems an enormously challenging and complex activity.System Verification3Hard- and Software VerificationSystem verification techniques are being applied to the design of ICT systems in a morereliable way.

Briefly, system verification is used to establish that the design or productunder consideration possesses certain properties. The properties to be validated can bequite elementary, e.g., a system should never be able to reach a situation in which noprogress can be made (a deadlock scenario), and are mostly obtained from the system’sspecification. This specification prescribes what the system has to do and what not,and thus constitutes the basis for any verification activity.

A defect is found once thesystem does not fulfill one of the specification’s properties. The system is consideredto be “correct” whenever it satisfies all properties obtained from its specification. Socorrectness is always relative to a specification, and is not an absolute property of asystem. A schematic view of verification is depicted in Figure 1.2.systemspecificationDesign Processpropertiesproduct orprototypebug(s) foundVerificationno bugs foundFigure 1.2: Schematic view of an a posteriori system verification.This book deals with a verification technique called model checking that starts from aformal system specification.

Before introducing this technique and discussing the roleof formal specifications, we briefly review alternative software and hardware verificationtechniques.Software Verification Peer reviewing and testing are the major software verificationtechniques used in practice.A peer review amounts to a software inspection carried out by a team of software engineersthat preferably has not been involved in the development of the software under review. The4System Verificationuncompiled code is not executed, but analyzed completely statically.

Empirical studiesindicate that peer review provides an effective technique that catches between 31 % and93 % of the defects with a median around 60%. While mostly applied in a rather ad hocmanner, more dedicated types of peer review procedures, e.g., those that are focused atspecific error-detection goals, are even more effective.

Despite its almost complete manualnature, peer review is thus a rather useful technique. It is therefore not surprising thatsome form of peer review is used in almost 80% of all software engineering projects. Dueto its static nature, experience has shown that subtle errors such as concurrency andalgorithm defects are hard to catch using peer review.Software testing constitutes a significant part of any software engineering project. Between30% and 50% of the total software project costs are devoted to testing.

As opposed to peerreview, which analyzes code statically without executing it, testing is a dynamic techniquethat actually runs the software. Testing takes the piece of software under considerationand provides its compiled code with inputs, called tests. Correctness is thus determinedby forcing the software to traverse a set of execution paths, sequences of code statementsrepresenting a run of the software. Based on the observations during test execution, theactual output of the software is compared to the output as documented in the systemspecification.

Although test generation and test execution can partly be automated, thecomparison is usually performed by human beings. The main advantage of testing is thatit can be applied to all sorts of software, ranging from application software (e.g., e-businesssoftware) to compilers and operating systems. As exhaustive testing of all execution pathsis practically infeasible; in practice only a small subset of these paths is treated. Testingcan thus never be complete. That is to say, testing can only show the presence of errors,not their absence.

Another problem with testing is to determine when to stop. Practically,it is hard, and mostly impossible, to indicate the intensity of testing to reach a certaindefect density – the fraction of defects per number of uncommented code lines.Studies have provided evidence that peer review and testing catch different classes of defects at different stages in the development cycle.

They are therefore often used together.To increase the reliability of software, these software verification approaches are complemented with software process improvement techniques, structured design and specificationmethods (such as the Unified Modeling Language), and the use of version and configuration management control systems. Formal techniques are used, in one form or another, inabout 10 % to 15% of all software projects. These techniques are discussed later in thischapter.Catching software errors: the sooner the better. It is of great importance to locate software bugs.

The slogan is: the sooner the better. The costs of repairing a software flawduring maintenance are roughly 500 times higher than a fix in an early design phase (seeFigure 1.3). System verification should thus take place early stage in the design process.System Verification5AnalysisConceptualDesignProgrammingUnit TestingSystem TestingOperation12.550%40%30%introducederrors (in %)detectederrors (in %)cost of10correctionper error(in 1,000 US $)7.520%510%2.500%Time (non-linear)Figure 1.3: Software lifecycle and error introduction, detection, and repair costs [275].About 50% of all defects are introduced during programming, the phase in which actualcoding takes place. Whereas just 15% of all errors are detected in the initial design stages,most errors are found during testing.

At the start of unit testing, which is oriented todiscovering defects in the individual software modules that make up the system, a defectdensity of about 20 defects per 1000 lines of (uncommented) code is typical. This hasbeen reduced to about 6 defects per 1000 code lines at the start of system testing, wherea collection of such modules that constitutes a real product is tested. On launching a newsoftware release, the typical accepted software defect density is about one defect per 1000lines of code lines1 .Errors are typically concentrated in a few software modules – about half of the modulesare defect free, and about 80% of the defects arise in a small fraction (about 20%) ofthe modules – and often occur when interfacing modules. The repair of errors that aredetected prior to testing can be done rather economically.

The repair cost significantlyincreases from about $ 1000 (per error repair) in unit testing to a maximum of about$ 12,500 when the defect is demonstrated during system operation only. It is of vitalimportance to seek techniques that find defects as early as possible in the software designprocess: the costs to repair them are substantially lower, and their influence on the restof the design is less substantial.Hardware Verification Preventing errors in hardware design is vital. Hardware issubject to high fabrication costs; fixing defects after delivery to customers is difficult, andquality expectations are high.

Whereas software defects can be repaired by providing1For some products this is much higher, though. Microsoft has acknowledged that Windows 95 containedat least 5000 defects. Despite the fact that users were daily confronted with anomalous behavior, Windows95 was very successful.6System Verificationusers with patches or updates – nowadays users even tend to anticipate and accept this –hardware bug fixes after delivery to customers are very difficult and mostly require refabrication and redistribution. This has immense economic consequences.

The replacementof the faulty Pentium II processors caused Intel a loss of about $ 475 million. Moore’slaw – the number of logical gates in a circuit doubles every 18 months – has proven tobe true in practice and is a major obstacle to producing correct hardware. Empiricalstudies have indicated that more than 50% of all ASICs (Application-Specific IntegratedCircuits) do not work properly after initial design and fabrication.