Handbook of Model Checking

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. This chapter is an introduction and short survey of model checking. The chapter aims to motivate and link the individual chapters of the handbook, and to provide context for readers who are not familiar with model checking.

Temporal logic has been used by philosophers to reason about the way the world changes over time. Its modern use in specification and verification of systems describes the evolution of states of a program/design giving rise to descriptions of executions. Temporal logics can be classified by their view of the evolution of time as either linear or branching. In the linear-time view, we see time ranging over a linear total order and executions are sequences of states. When the system has multiple possible executions (due to nondeterminism or reading input) we view them as separate possible evolutions and the system has a set of possible behaviors. In the branching-time view, a point in time may have multiple possible successors and accordingly executions are tree-like structures. According to this view, a system has exactly one execution, which takes the form of a tree. We start this chapter by introducing Fair Discrete Structures, the model on which we evaluate the truth and falsity of temporal logic formulas. Fair Discrete Structures describe the states of a system and their possible evolution. We then proceed with the linear-time view and introduce Propositional Linear Temporal Logic (LTL). We explain the distinction between safety and liveness properties and introduce a hierarchy of liveness properties of increasing expressiveness. We study the expressive power of full LTL and cover extensions that increase its expressive power. We introduce algorithms for checking the satisfiability of LTL and model checking LTL. We turn to the branching-time framework and introduce Computation Tree Logic (CTL). As before, we discuss its expressive power, consider extensions, and cover satisfiability and model checking. We then dedicate some time to examples of formulas in both LTL and CTL and stress the differences between the two. We end with a formal comparison of LTL and CTL and, in view of this comparison, introduce CTL*, a hybrid of LTL and CTL that combines the linear and branching views into one logic.

System modeling is the initial, and often crucial, step in verification. The right choice of model and modeling language is important for both designers and users of verification tools. This chapter aims to provide a guide to system modeling in four stages. First, it provides an overview of the main issues one must consider in modeling systems for verification. These issues involve both the selection or design of a modeling language and the steps of model creation. Next, it introduces a simple modeling language, sml, for illustrating the issues involved in selecting or designing a modeling language. sml uses an abstract state machine formalism that captures key features of widely-used languages based on transition system representations. We introduce the simple modeling language to simplify the connection between languages used by practitioners (such as Verilog, Simulink, or C) and various underlying formalisms (e.g., automata or Kripke structures) used in model checking. Third, the chapter demonstrates key steps in model creation using sml with illustrative examples. Finally, the presented modeling language sml is mapped to standard formalisms such as Kripke structures.

We study automata on infinite words and their applications in system specification and verification. We first introduce Büchi automata and survey their closure properties, expressive power, and determinization. We then introduce additional acceptance conditions and the model of alternating automata. We compare the different classes of automata in terms of expressive power and succinctness, and describe decision problems for them. Finally, we describe the automata-theoretic approach to system specification and verification.

In this chapter we discuss the methodology used in explicit-state logic model checking, specifically as applied to asynchronous software systems. As the name indicates, in an explicit-state model checker the state descriptor for a system is maintained in explicit, and not symbolic, form, as are all state transitions. Abstraction techniques and partial-order reduction algorithms are used to reduce the search space to a minimum, and advanced storage techniques can be used to extend the reach of this form of verification to very large system sizes. The basic algorithms for explicit-state model checking date from the late 1970s and early 1980s. More advanced versions of these algorithms remain an active area of research.

Partial order reduction methods help reduce the time and space required to automatically verify concurrent asynchronous systems based on commutativity between concurrently executed transitions. We describe partial order reduction for various specification formalisms, such as LTL, CTL, and process algebra.

Binary decision diagrams provide a data structure for representing and manipulating Boolean functions in symbolic form. They have been especially effective as the algorithmic basis for symbolic model checkers. A binary decision diagram represents a Boolean function as a directed acyclic graph, corresponding to a compressed form of decision tree. Most commonly, an ordering constraint is imposed among the occurrences of decision variables in the graph, yielding ordered binary decision diagrams (OBDD). Representing all functions as OBDDs with a common variable ordering has the advantages that (1) there is a unique, reduced representation of any function, (2) there is a simple algorithm to reduce any OBDD to the unique form for that function, and (3) there is an associated set of algorithms to implement a wide variety of operations on Boolean functions represented as OBDDs. Recent work in this area has focused on generalizations to represent larger classes of functions, as well as on scaling implementations to handle larger and more complex problems.

Symbolic model checking based on Binary Decision Diagrams (BDDs) is one of the most celebrated breakthroughs in the area of formal verification. It was originally proposed in the context of hardware model checking, and advanced the state of the art in model-checking capability by several orders of magnitude in terms of the sizes of state spaces that could be explored successfully. More recently, it has been extended to the domain of software verification as well, and several BDD-based model checkers for Boolean programs and push-down systems have been developed. In this chapter, we summarize some of the key concepts and techniques that have emerged in this story of successful practical verification.

The Boolean Satisfiability Problem (SAT) is well known in computational complexity, representing the first decision problem to be proved NP-complete. SAT is also often the subject of work in proof complexity. Besides its theoretical interest, SAT finds a wide range of practical applications. Moreover, SAT solvers have been the subject of remarkable efficiency improvements since the mid-1990s, motivating their widespread use in many practical applications including Bounded and Unbounded Model Checking. The success of SAT solvers has also motivated the development of algorithms for natural extensions of SAT, including Quantified Boolean Formulas (QBF), Pseudo-Boolean constraints (PB), Maximum Satisfiability (MaxSAT) and Satisfiability Modulo Theories (SMT) which also see application in the model-checking context. This chapter first covers the organization of modern conflict-driven clause learning (CDCL) SAT solvers, which are used in the vast majority of practical applications of SAT. It then reviews the techniques shown to be effective in modern SAT solvers.

Modern satisfiability (SAT) solvers have become the enabling technology of many model checkers. In this chapter, we will focus on those techniques most relevant to industrial practice. In bounded model checking (BMC), a transition system and a property are jointly unwound for a given number k$k$ of steps to obtain a formula that is satisfiable if there is a counterexample for the property up to length k$k$. The formula is then passed to an efficient SAT solver. The strength of BMC is refutation: BMC has been used to discover subtle flaws in digital systems. We cover the application of BMC to both hardware and software systems, and to hardware/software co-verification. We also discuss means to make BMC complete, including k$k$-induction, Craig interpolation, abstraction refinement techniques, and inductive techniques with iterative strengthening.

Satisfiability Modulo Theories (SMT) refers to the problem of determining whether a first-order formula is satisfiable with respect to some logical theory. Solvers based on SMT are used as back-end engines in model-checking applications such as bounded, interpolation-based, and predicate-abstraction-based model checking. After a brief illustration of these uses, we survey the predominant techniques for solving SMT problems with an emphasis on the lazy approach, in which a propositional satisfiability (SAT) solver is combined with one or more theory solvers. We discuss the architecture of a lazy SMT solver, give examples of theory solvers, show how to combine such solvers modularly, and mention several extensions of the lazy approach. We also briefly describe the eager approach in which the SMT problem is reduced to a SAT problem. Finally, we discuss how the basic framework for determining satisfiability can be extended with additional functionality such as producing models, proofs, unsatisfiable cores, and interpolants.

State Explosion is a fundamental challenge for model checking methods. This term refers to the potentially exponential growth of the state space of a program as a function of the number of its components. Compositional reasoning is a technique which aims to ameliorate the effects of state explosion. In its essence, it replaces reasoning on the global state space of a program with localized reasoning: each component is analyzed separately, based on assumptions about the behavior of the other components. The challenge for a fully automated method is the construction of the right assumptions: they should be strong enough to prove a desired property, while being simple enough for efficient analysis. This chapter describes the ideas underlying compositional reasoning, foundational algorithms for generating assumptions, and applications.

Abstraction, in the context of model checking, is aimed at reducing the state space of the system by omitting details that are irrelevant to the property being verified. Many successful approaches to the “state explosion problem,” some of them described in other chapters, can be seen as abstractions. In this chapter, several notions of abstraction are considered in a uniform setting. Different such notions lead to a variety of preservation results that establish which kind of temporal properties may be verified via an abstracted system. We first define the needed background on simulation and bisimulation relations and their logic preservation. We then present the abstraction that is currently most widely used in practice: existential abstraction, which preserves universal fragments of branching-time logics. We give examples of such abstractions: localization reduction for hardware and predicate abstraction for software. We then proceed to stronger abstractions which preserve full branching-time logics. We introduce Kripke Modal Transition Systems and modal simulation, and show logic preservation. We close the chapter with a review of the presented results in the light of the notion of completeness.

In this chapter we consider applications of logical proofs in model checking. Here we are not concerned with using model checking to verify steps in a larger proof but rather with ways in which logical proof methods can aid model checking, particularly in focusing model-checking methods on relevant facts. We introduce a framework for abstraction refinement based on a concept of deductive generalization. We then show how various abstraction refinement schemes can be understood in this framework in terms of local proofs and Craig interpolation. This unifying view exposes the trade-offs made in different systems between the quality and cost of refinements, and also leads to novel model-checking approaches.

We present basic principles of algorithms for the verification of safety and termination of programs. The algorithms call procedures on logical formulas in order to construct an abstraction and to refine an abstraction. The two underlying concepts are predicate abstraction and counterexample-guided abstraction refinement.

Until recently, model checking and data-flow analysis—two traditional approaches to software verification—were used independently and in isolation for solving similar problems. Theoretically, the two different approaches are equivalent; they are two different ways to compute the same solution to a problem. In recent years, new practical approaches have shown how to combine the approaches and how to make them benefit from each other—model-checking techniques can make data-flow analyses more precise, and data-flow-analysis techniques can make model checking more efficient. This chapter starts by discussing the relationship (differences and similarities) between type checking, data-flow analysis, and model checking. Then we define algorithms for data-flow analysis and model checking in the same formal setting, called configurable program analysis. This identifies key differences that make us call an algorithm a “model-checking” algorithm or a “data-flow-analysis” algorithm. We illustrate the effect of using different algorithms for running certain classic example analyses and point out the reason for one algorithm being “better” than the other. The chapter presents combined verification techniques in the framework of configurable program analysis, in order to emphasize techniques used in data-flow analysis and in model checking. Besides the iterative algorithm that is used to illustrate the similarities and differences between data-flow analysis and model checking, we discuss different algorithmic approaches for constructing program invariants. To show that the border between data-flow analysis and model checking is blurring and disappearing, we also discuss directions in tool implementations for combined verification approaches.

We consider the model-checking problem for sequential programs with procedure calls. We first present basic algorithms for solving the reachability problem and the fair computation problem. The algorithms are based on two techniques: summarization, which computes reachability information by solving a set of fixpoint equations, and saturation, which computes the set of all reachable program states (including call stacks) using automata. Then, we study formalisms to specify requirements of programs with procedure calls. We present an extension of Linear Temporal Logic allowing propagation of information across the hierarchical structure induced by procedure calls and matching returns. Finally, we show how model checking can be extended to this class of programs and properties.

Concurrent programs are in widespread use for harnessing the computing power of multi-core hardware. However, it is very challenging to develop correct concurrent programs. In practice, concurrency-related bugs such as data races, deadlocks, and atomicity violations are very common. In this chapter, we describe efforts based on model-checking for automatic verification and debugging of concurrent programs. The emphasis is on core ideas for reasoning about synchronizations and communication between threads and processes, while considering all possible behaviors due to their interactions.We start by considering model-checking based on interacting pushdown system (PDS) models. In these models, each component (thread or process) is modeled as a pushdown automaton, where the stack is used to model recursion. Model checking based on pushdown automata has a close correspondence with dataflow analysis of programs, and this has been successfully used for verification of sequential programs. However, applying these methods to a system of interacting pushdown automata is not straightforward. Even the basic problem of reachability is undecidable in the general case. We describe some techniques that have been proposed to get around this barrier, by restricting the patterns of synchronization and communication among components.Although PDSs provide a natural model for concurrent programs, it is difficult to apply PDS-based model-checking techniques directly to concurrent programs in practice. In addition to the formidable decidability barrier, this is also due to the huge gap between low-level PDS models and the feature-rich high-level programming languages in which concurrent programs are written. Fortunately, the successes of model-checking on finite state systems and sequential programs have provided a wealth of useful abstractions and techniques to bridge this gap. In the last part of the chapter, we will describe verification techniques for concurrent programs that are inspired by these models. They often abstract the effects of synchronization and focus on handling the complexity of reasoning about all possible behaviors. However, they can, and should, exploit insights and results of PDS-based model-checking.

Model checking and testing have a lot in common. Over the last two decades, significant progress has been made on how to broaden the scope of model checking from finite-state abstractions to actual software implementations. One way to do this consists of adapting model checking into a form of systematic testing that is applicable to industrial-size software. This chapter presents an overview of this strand of software model checking.

There are two basic approaches to automated verification. In model checking, the system is viewed as a graph representing possible execution steps. Properties are established by exploring or traversing the graph structure. In deduction, both the system and its putative properties are represented by formulas in a logic, and the resulting proof obligations are discharged by decision procedures or by automated or semi-automated proof construction. Model checking sacrifices expressivity for greater automation, and with deduction it is vice versa. Newer techniques combine deductive and model-checking approaches to achieve greater scale, expressivity, and automation. We examine the logical foundations of the two approaches and explore their similarities, differences, and complementarities. The presentation is directed at students and researchers who are interested in understanding the research challenges at the intersection of deduction and model checking.

We consider the model-checking problem for a particular class of parameterized systems: systems that consist of arbitrary numbers of components. The task is to show correctness regardless of the number of components. The term parameterized refers to the fact that the size of the system is a parameter of the verification problem. Examples of parameterized systems include mutual exclusion algorithms, bus protocols, networking protocols, cache coherence protocols, web services, and sensor networks. In this chapter, we will give four examples of techniques that have been used (among many others) for the verification of parameterized systems.

The formal analysis of security protocols is a prime example of a domain where model checking has been successfully applied. Although security protocols are typically small, analysis by hand is difficult as a protocol should work even when arbitrarily many runs are interleaved and in the presence of an adversary. Specialized model-checking techniques have been developed that address both the problems of unbounded, interleaved runs and a prolific, highly nondeterministic adversary. These techniques have been implemented in model-checking tools that now scale to protocols of realistic size and can be used to aid protocol design and standardization.In this chapter, we provide an overview of the main applications of model checking in security protocol analysis. We explain the central concepts involved in the analysis of security protocols: the abstraction of messages, protocols as role automata, the adversary model, and property specification. We explain and relate the main algorithms used and describe systems based on them. We also give examples of the successful applications of model checking to protocol standards. Finally, we provide an outlook on the field: What is possible with the state of the art and what are the future challenges?

This chapter traces the practical challenges that were overcome in order to transfer model-checking theory to industrial practice. In retrospect, this transfer provided a lesson in how to, and how not to accomplish technology transfer. The methodology changes required for industrial model checking were achieved through a succession of steps, each of which was small enough to avoid unacceptable disruption of existing methodologies, while significant enough to demonstrate value.

In the late 1970s, Amir Pnueli suggested that functional properties of reactive systems be formally expressed in temporal logic. For model checking such a logic to be possible, it must have sufficient expressive power, its semantics must be formally defined in a rigorous way, and the complexity of model checking it must be well understood and reasonable. In order to allow widespread adoption in industry, there is an additional requirement: functional specification must be made easy, allowing common properties to be expressed intuitively and succinctly. But while adding syntax is simple, defining semantics without breaking properties of the existing semantics is a different story. This chapter is about the various extensions to temporal logic included in the IEEE standards PSL and SVA, their motivation, and the subtle semantic issues encountered in their definition.

Symbolic trajectory evaluation is an industrial-strength formal hardware verification method, based on symbolic simulation, which has been highly successful in data-path verification, especially for microprocessor execution units. It is a ‘model-checking’ method in the basic sense that properties, expressed in a simple temporal logic, are verified by (symbolic) exploration of formal models of sequential circuits. Its defining characteristic is that it operates by symbolic simulation over abstractions of sets of states that only partially delineate the circuit states in the set. These abstract state sets are ordered in a lattice by information content, based on a three-valued domain for values on circuit nodes (true, false, and don’t know). The algorithm operates over families of these abstractions encoded by Boolean formulas, providing a flexible, specification-driven mechanism for partitioned data abstraction. We provide a basic introduction to symbolic trajectory evaluation and its extensions, and some details of how it is deployed in industrial practice. The aim is to get across the essence and value of the method in clear and accessible terms.

This chapter presents that part of the theory of the μ$\mu$-calculus that is relevant to the model-checking problem as broadly understood. The μ$\mu$-calculus is one of the most important logics in model checking. It is a logic with an exceptional balance between expressiveness and algorithmic properties.The chapter describes at length the game characterization of the semantics of the μ$\mu$-calculus. It discusses the theory of the μ$\mu$-calculus starting with the tree-model property, and bisimulation invariance. Then it develops the notion of modal automaton: an automaton-based model behind the μ$\mu$-calculus. It gives a quite detailed explanation of the satisfiability algorithm, followed by results on alternation hierarchy, proof systems, and interpolation. Finally, the chapter discusses the relation of the μ$\mu$-calculus to monadic second-order logic as well as to some program and temporal logics. It also presents two extensions of the μ$\mu$-calculus that allow us to address issues such as inverse modalities.

Graph-based games are an important tool in computer science. They have applications in synthesis, verification, refinement, and far beyond. We review graph-based games with objectives on infinite plays. We give definitions and algorithms to solve the games and to give a winning strategy. The objectives we consider are mostly Boolean, but we also look at quantitative graph-based games and their objectives. Synthesis aims to turn temporal logic specifications into correct reactive systems. We explain the reduction of synthesis to graph-based games (or equivalently tree automata) using synthesis of LTL specifications as an example. We treat the classical approach that uses determinization of parity automata and more modern approaches.

The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap. 2), and subsequently extended to also handle quantitative features, such as real time (see Chap. 29), continuous flows (see Chap. 30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains.

This chapter surveys timed automata as a formalism for model checking real-time systems. We begin with introducing the model, as an extension of finite-state automata with real-valued variables for measuring time. We then present the main model-checking results in this framework, and give a hint about some recent extensions (namely weighted timed automata and timed games).

Hybrid systems are models which combine discrete and continuous behavior. They occur frequently in safety-critical applications in various domains such as health care, transportation, and robotics, as a result of interactions between a digital controller and a physical environment. They also have relevance in other areas such as systems biology, in which the discrete dynamics arises as an abstraction of fast continuous processes. One of the prominent models is that of hybrid automata, where differential equations are associated with each node, and jump constraints such as guards and resets are associated with each edge.In this chapter, we focus on the problem of model checking of hybrid automata against reachability and invariance properties, enabling the verification of general temporal logic specifications. We review the main decidability results for hybrid automata, and since model checking is in general undecidable, we present three complementary analysis approaches based on symbolic representations, abstraction, and logic. In particular, we illustrate polyhedron-based reachability analysis, finite quotients, abstraction refinement techniques, and logic-based verification. We survey important tools and application domains of successful hybrid system verification in this vibrant area of research.

We consider symbolic model checking as a general procedure to compute fixed points on general lattices. We show that this view provides a unified approach for formal reasoning about systems that is applicable to many different classes of systems and properties. Our unified view is based on the notion of region algebras together with appropriate generalizations of the modal μ$\mu$-calculus. We show applications of our general approach to problems in infinite-state verification, reactive synthesis, and the analysis of probabilistic systems.

Process algebras such as CCS, CSP and ACP are abstract notations for describing concurrent systems that interact via (usually) handshake-based communication. They lead to natural concepts of process state and are therefore natural candidates for model checking. We survey the area of process algebra and model checking, focusing on these three process algebras. We first introduce the syntax and semantics of these process algebras, before looking at the algorithmic basis for their model checking, which includes ideas such as bisimulation and refinement as well as the logics used to describe system-correctness properties. Finally, we introduce the process-alebra-based model-checking tools FDR, CWB and XMC, illustrating their utility by a number of case studies.