126 MODEL CHECKING OF FINITE-STATE SYSTEMS

procedure TTG min delay(start set, final set)

time counter := 0 for every s, time counter start set;

reachable set := set of states s, t reachable from start set in t time units; min delay(start set, final set);

Figure 4.10 TTG minimum delay algorithm.

This means that in the augmented transition relation Na , there is a transition froms, t to s , t iff there is a transition from state s to state s in the original transition relation N , and either s belongs to the condition and the counter t is t + d or s does not belongs to the condition and t is the same as t. This transition relation increments the time counter only when the state s belongs to the condition. Therefore, a path exists with t time units spent in states belonging to condition along this path from a state in start set to state s if an augmented state s, t is reachable from start set.

4.8 AVAILABLE TOOLS

Several versions of SMV (symbolic model verifier) are available, two of which are from the Carnegie Mellon University (CMU) Model Checking group and Cadence Berkeley Laboratories. TCMU’s SMV is the first model checker based on BDDs. Their respective URLs are

http://www.cs.cmu.edu/~modelcheck/smv.html

http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/

CMU’s SMV takes as input a specification (called a program) consisting of several modules. A module is a description that may be instantiated several times within the model. Every SMV specification has a module called main with no formal parameters, which form the root of the model hierarchy. The main module is the starting point for building the finite-state model for a given description. A declaration

MODULE process( p1, . . . , pn)

defines process as a module with n formal parameters.

Local variables may be declared in a module. The type of variable may be Boolean, an enumeration type or an integer subrange. For example, the values of the following local variable state1 can be gate up or gate down:

VAR state1: gate up, gate down;

Modules are also instantiated using variable declarations. A module may contain instances of other modules, allowing a structural hierarchy to be built. For example, the module main declares the variable p0 as an instance of proc

VAR p0: proc(s0, s1, turn, 0);

The init and next functions define the values of the variables in each state, as shown in the following example showing a partial description of the automatic climate control system in Figure 2.13 in chapter 2:

init(state0) := comfort; next(state0) := case

(state0 = comfort): {cold, hot, comfort}; (state0 = cold) : turn_on_heater;

(state0 = hot) : turn_on_ac;

...

esac;

The code above defines the initial value of state0 to be comfort, and the value of that variable in the next state as a function of the value of the variables in the current state. If state0 is comfort, then in the next state its value could be cold, hot, or comfort, and the choice is made nondeterministically. If state0 is cold, then in the next state its value is turn on heater. If state0 is hot, then in the next state its value is turn on ac. The operators & (AND) and | (OR) can be used to express more complex conditions on state values.

SyMP (symbolic model prover) is a new tool combining model checking and theorem proving to facilitate verification. More details about SyMP can be found in

http://www.cs.cmu.edu/~modelcheck/symp.html

Recently, a new symbolic model checker called NuSMV has been developed as a joint project between the Formal Methods group in the Automated Reasoning System division at Italy’s ITC-IRST and the Model Checking group at Carnegie Mellon University. NuSMV is a reimplementation and extension of SMV, and can be found at

http://nusmv.irst.itc.it/

The open architecture of NuSMV for model checking makes it a reliable core for developing custom verification tools, verifying industrial designs, and serving as a testbed for formal verification techniques.

4.9 HISTORICAL PERSPECTIVE AND RELATED WORK

Clarke and Emerson first developed analysis algorithms called temporal logic model checkers to verify desirable properties of untimed systems specified as finite state machines [Clarke and Emerson, 1981; Clarke, Emerson, and Sistla, 1986]. To reduce the run time for model checking, Burch et al. [Burch et al., 1990a] and McMillan [McMillan, 1992] invented symbolic model checking algorithms in which the transition relation is represented by a binary decision diagram (BDD) [Lee, 1959; Akers, 1978; Bryant, 1986] so that states are not explicitly enumerated, thus significantly

128 MODEL CHECKING OF FINITE-STATE SYSTEMS

reducing verification time. BDDs were first invented by Lee [Lee, 1959] and later refined by Akers [Akers, 1978]. To further combat the problem of checking large specifications, Sokolsky and Smolka recently proposed incremental model checking [Sokolsky and Smolka, 1994] and local model checking [Sokolsky and Smolka, 1995]. These model checkers explore only the portion of the state space responsible in determining the outcome of the verification. Recently, Amla, Emerson, Kurshan, and Namjoshi [Amla and Emerson, 2001] presented a front-end called RTDT for the efficient model checking of synchronous timing diagrams.

Burch models timing constraints with trace theory [Burch, 1989a], and adds timing specification capability to CTL by combining CTL, trace theory, and timing models [Burch, 1989b]. Burch et al. apply symbolic model checking to sequential circuit verification [Burch et al., 1990a; Burch et al., 1994], and to problems with large state spaces [Burch et al., 1990a]. McMillan [McMillan, 1992] uses the SMV to check several industrial specifications, including the IEEE Futurebus+ cache coherence protocol [Clarke et al., 1993]. Cleaveland and others implement an integrated toolset called the Concurrency Factory [Cleaveland et al., 1994] to specify and verify concurrent systems. This toolset is based on their earlier toolset called the Concurrency Workbench [Cleaveland, Parrow, and Steffen, 1993].

To further tackle the state explosion problem, [Henzinger, Kupferman, and Vardi, 1996] present an automata-theoretic approach to TCTL (a real-time extension of CTL) model checking that combines on-the-fly and space-efficient model checking methods. Their approach yields a PSPACE on-the-fly model-checking algorithm for TCTL. On-the-fly model checking explores only the portion of the state space that is essential for determining the satisfaction of the specification. Space-efficient model checking uses extra time to reconstruct information rather than using extra space to store it.

[Campos et al., 1994] apply symbolic model checking to real-time systems by introducing quantitative algorithms for computing minimum and maximum delays between two events and for calculating the minimum and maximum number of times a given condition holds between two events or sets of states. The length of a path is in terms of the number of transitions in it. To demonstrate the capability of these techniques, they apply them to verify timing properties of aircraft control. They generalize this definition in their timed transition graphs [Campos and Clarke, 1993] to allow a transition to model the passage of more than one unit of time. Furthermore, the time taken by a transition may be different for different executions of the same modeled system.

[Iversen et al., 2000] use model-checking to verify real-time control programs. [Closse, et al., 2001] provide a tool called TAXYS for the development and verification of real-time embedded systems. [Havelund, Lowry, and Penix, 2001] present a formal analysis of a spacecraft controller using the tool SPIN.

Recently, [Kupferman and Vardi, 2000] proposed an automata-theoretic approach to modular model checking and dealt with assume-guarantee specifications with the guarantee specified by branching temporal formulas. The specification of a module in modular verification, also called the assume-guarantee paradigm, consists of describing the guaranteed behavior of the module and the assumed behavior of the

SUMMARY 129

system in which the module is interacting. They consider two approaches, one in which the assumption is specified by branching temporal formulas and the other in which the assumption is specified by linear temporal logic. Guarantees are specified in CTL, and CTL*.

[Browne, Cheng, and Mok, 1988; Cheng and Wang, 1990; Cheng et al., 1993] incorporated a modified model checker in the analysis tool Estella (described in chapter 10) for determining whether a real-time rule-based system has bounded response time. This modified model checker also computes the worst-case response time of a rule-based system by finding the longest path in terms of the number of edges from a start state to a fixed point. If the response time of the rule-base system is bounded, Estella also finds its worst-case response time. The implemented model checker also makes use of on-the-fly and space-efficient techniques. Estella employs semanticsbased analysis and avoids model checking if the rule-based system being checked satisfies certain constraints, thus dramatically reducing the analysis time.

4.10 SUMMARY

For finite-state concurrent systems, we can use model checking instead of proof construction to check their correctness relative to their specifications. In the model checking approach, we represent the concurrent system as a finite-state graph, which can be viewed as a finite Kripke structure. The specification or safety assertion is expressed in propositional temporal logic formulas. We can then check whether the system meets its specification using an algorithm called a model checker. In other words, the model checker determines whether the Kripke structure is a model of the formula(s). Several model checkers are available and they vary in code and run-time complexity. Here we describe one of the first model checkers proposed by [Clarke, Emerson, and Sistla, 1986], and a more efficient symbolic model checker developed later by [Burch et al., 1990a].

In Clarke, Emerson, and Sistla’s approach, the system to be checked is represented by a labeled finite-state graph and the specification is written in a propositional, branching-time temporal logic called computation tree logic (CTL). The use of linear-time temporal logic, which can express fairness properties, is ruled out since a model checker for such logic has high complexity. Instead, fairness requirements are moved into the semantics of CTL.

One way to construct the finite-state graph corresponding to a given concurrent program is to begin with the initial state labeled with the initial values of all program variables or attributes, which are called labels here. Then for each possible next statement, we execute the statement and examine if any change occurs to one or more program variables. We construct a new state if it is different from any existing state. Note that sometimes we need to construct a new state even if its labels are the same as those in an existing state because the sequence of actions leading to the present state is different from that leading to the existing state. A directed edge is constructed from the state we are considering to the new state. We repeat this

130 MODEL CHECKING OF FINITE-STATE SYSTEMS

state and edge construction step for each new state until there are no more states to consider.

For other systems that are not computer programs, we can perform a similar graph construction. First, we identify the state attributes that are relevant in the system to be specified in the CTL structure.

The Clarke–Emerson–Sistla (CES) model checker can determine whether a formula f0 written in CTL is true in a given CTL structure. It uses a compositional approach to analysis and hence operates in stages. The first stage checks all subformulas of length 1 in f0, that is, all atomic propositions. These atomic propositions hold in states having labels that are identical to these propositions. The second stage checks all subformulas of length 2 in f0 based on the results in stage 1 and labels each state with the subformulas that hold in that state, and so on. As a result, each state will be labeled with the set of subformulas of length less than or equal to i after the completion of the ith stage. At completion, the model checker will have checked the entire formula of length n.

The CES model checker and other early model checkers are explicit-state model checkers. They represent a finite-state graph using adjacency lists and explicitly list all states in the graph. Since many models have an exponential number of states, explicit-state model checkers suffer from the state explosion problem and are not practical for the verification of many realistic systems. To alleviate this problem, symbolic model checking [Burch et al., 1990a] is introduced, which represents states and transitions as Boolean formulas in order to reduce redundancy in the graph. These Boolean formulas are then represented by even more compact binary decision diagrams (BDDs) [Lee, 1959; Akers, 1978], which can then be manipulated by very efficient algorithms [Bryant, 1986]. As a result, symbol model checking makes it practical to verify much larger systems than those analyzable by explicit-state model checking.

BDDs are concise graphical representations of Boolean formulas. Boolean logic formulas can be represented by truth tables, Karnaugh maps, or canonical sum-of- products forms, but these representations contain redundant information in different places, leading to an exponential number of entries or states.

A Boolean formula can be represented by a function graph (ordered BDD), which is a rooted, directed, acyclic graph with two types of vertices. A nonterminal vertex v has an index(v) from the set {1, . . . , n} and two children low(v) and high(v). A terminal vertex (leaf) has a value(v) of 0 or 1. If low(v) is a nonterminal vertex, then index(v) < index(low(v)). Similarly, if high(v) is a nonterminal vertex, then index(v) < index(high(v)).

Besides being much more compact that other representations, ordered BDDs are canonical representations of Boolean formulas. This property means that each Boolean formula with a specific variable ordering has a unique and minimal BDD representation. In fact, BDDs can be viewed as deterministic finite automata (DFA), discussed in chapter 2. Therefore, we can check that two Boolean formulas are equivalent by checking if they have isomorphic representations, that is, their BDDs match exactly in both structure and attributes. Also, determining the satisfiability of a formula only requires comparing its BDD with that of the constant function false (0).