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

The book will therefore be the ideal choice as a textbook forboth graduate and advanced undergraduate students, as well as for self-study, and shoulddefinitely be on the bookshelf of any researcher interested in the topic.Kim Guldstrand LarsenProfessor in Computer ScienceAalborg University, DenmarkMay 2007PrefaceIt is fair to state, that in this digital eracorrect systems for information processingare more valuable than gold.(H. Barendregt. The quest for correctness.In: Images of SMC Research 1996, pages 39–58, 1996.)This book is on model checking, a prominent formal verification technique for assessing functional properties of information and communication systems.

Model checkingrequires a model of the system under consideration and a desired property and systematically checks whether or not the given model satisfies this property. Typical propertiesthat can be checked are deadlock freedom, invariants, and request-response properties.Model checking is an automated technique to check the absence of errors (i.e., propertyviolations) and alternatively can be considered as an intelligent and effective debuggingtechnique. It is a general approach and is applied in areas like hardware verification andsoftware engineering.

Due to unremitting improvements of underlying algorithms and datastructures together with hardware technology improvements, model-checking techniquesthat two decades ago only worked for simple examples are nowadays applicable to morerealistic designs. It is fair to say that in the last two decades model checking has developedas a mature and heavily used verification and debugging technique.Aims and ScopeThis book attempts to introduce model checking from first principles, so to speak, and isintended as a textbook for bachelor and master students, as well as an introductory bookfor researchers working in other areas of computer science or related fields.

The readeris introduced to the material by means of an extensive set of examples, most of whichare examples running throughout several chapters. The book provides a complete set ofbasic results together with all detailed proofs. Each chapter is concluded by a summary,xvxviPrefacebibliographic notes, and a series of exercises, of both a theoretical and of a practical nature(i.e., experimenting with actual model checkers).PrerequisitesThe concepts of model checking have their roots in mathematical foundations such aspropositional logic, automata theory and formal languages, data structures, and graphalgorithms.

It is expected that readers are familiar with the basics of these topics whenstarting with our book, although an appendix is provided that summarizes the essentials.Knowledge on complexity theory is required for the theoretical complexity considerationsof the various model-checking algorithms.ContentThis book is divided into ten chapters. Chapter 1 motivates and introduces model checking. Chapter 2 presents transition systems as a model for software and hardware systems.Chapter 3 introduces a classification of linear-time properties into safety and liveness,and presents the notion of fairness. Automata-based algorithms for checking (regular)safety and ω-regular properties are presented in Chapter 4.

Chapter 5 deals with LinearTemporal Logic (LTL) and shows how the algorithms of Chapter 4 can be used for LTLmodel checking. Chapter 6 introduces the branching-time temporal logic ComputationTree Logic (CTL), compares this to LTL, and shows how to perform CTL model checking, both explicitly and symbolically. Chapter 7 deals with abstraction mechanisms thatare based on trace, bisimulation, and simulation relations. Chapter 8 treats partial-orderreduction for LTL and CTL. Chapter 9 is focused on real-time properties and timed automata, and the monograph is concluded with a chapter on the verification of probabilisticmodels.

The appendix summarizes basic results on propositional logic, graphs, language,and complexity theory.How to Use This BookA natural plan for an introductory course into model checking that lasts one semester(two lectures a week) comprises Chapters 1 through 6. A follow-up course of about asemester could cover Chapters 7 through 10, after a short refresher on LTL and CTLmodel checking.PrefacexviiAcknowledgmentsThis monograph has been developed and extended during the last five years.

The followingcolleagues supported us by using (sometimes very) preliminary versions of this monograph:Luca Aceto (Aalborg, Denmark and Reykjavik, Iceland), Henrik Reif Andersen (Copenhagen, Denmark), Dragan Boshnacki (Eindhoven, The Netherlands), Franck van Breughel(Ottawa, Canada), Josée Desharnais (Quebec, Canada), Susanna Donatelli (Turin, Italy),Stefania Gnesi (Pisa, Italy), Michael R. Hansen (Lyngby, Denmark), Holger Hermanns(Saarbrücken, Germany), Yakov Kesselman (Chicago, USA), Martin Lange (Aarhus, Denmark), Kim G.

Larsen (Aalborg, Denmark), Mieke Massink (Pisa, Italy), Mogens Nielsen(Aarhus, Denmark), Albert Nymeyer (Sydney, Australia), Andreas Podelski (Freiburg,Germany), Theo C. Ruys (Twente, The Netherlands), Thomas Schwentick (Dortmund,Germany), Wolfgang Thomas (Aachen, Germany), Julie Vachon (Montreal, Canada), andGlynn Winskel (Cambridge, UK). Many of you provided us with very helpful feedbackthat helped us to improve the lecture notes.Henrik Bohnenkamp, Tobias Blechmann, Frank Ciesinski, Marcus Grösser, Tingting Han,Joachim Klein, Sascha Klüppelholz, Miriam Nasfi, Martin Neuhäusser, and Ivan S.

Zapreevprovided us with many detailed comments, and provided several exercises. Yen Cao iskindly thanked for drawing a part of the figures and Ulrich Schmidt-Görtz for his assistancewith the bibliography.Many people have suggested improvements and pointed out mistakes. We thank everyonefor providing us with helpful comments.Finally, we thank all our students in Aachen, Bonn, Dresden, and Enschede for theirfeedback and comments.Christel BaierJoost-Pieter KatoenChapter 1System VerificationOur reliance on the functioning of ICT systems (Information and Communication Technology) is growing rapidly. These systems are becoming more and more complex and aremassively encroaching on daily life via the Internet and all kinds of embedded systemssuch as smart cards, hand-held computers, mobile phones, and high-end television sets.In 1995 it was estimated that we are confronted with about 25 ICT devices on a dailybasis. Services like electronic banking and teleshopping have become reality.

The dailycash flow via the Internet is about 1012 million US dollars. Roughly 20% of the productdevelopment costs of modern transportation devices such as cars, high-speed trains, andairplanes is devoted to information processing systems. ICT systems are universal and omnipresent.

They control the stock exchange market, form the heart of telephone switches,are crucial to Internet technology, and are vital for several kinds of medical systems. Ourreliance on embedded systems makes their reliable operation of large social importance.Besides offering a good performance in terms like response times and processing capacity,the absence of annoying errors is one of the major quality indications.It is all about money. We are annoyed when our mobile phone malfunctions, or whenour video recorder reacts unexpectedly and wrongly to our issued commands. Thesesoftware and hardware errors do not threaten our lives, but may have substantial financialconsequences for the manufacturer.

Correct ICT systems are essential for the survival ofa company. Dramatic examples are known. The bug in Intel’s Pentium II floating-pointdivision unit in the early nineties caused a loss of about 475 million US dollars to replacefaulty processors, and severely damaged Intel’s reputation as a reliable chip manufacturer.The software error in a baggage handling system postponed the opening of Denver’s airportfor 9 months, at a loss of 1.1 million US dollar per day. Twenty-four hours of failure of12System VerificationFigure 1.1: The Ariane-5 launch on June 4, 1996; it crashed 36 seconds after the launchdue to a conversion of a 64-bit floating point into a 16-bit integer value.the worldwide online ticket reservation system of a large airplane company will cause itsbankruptcy because of missed orders.It is all about safety: errors can be catastrophic too.