EXERCISES 131

Instead of explicitly enumerating all states in the model, which is a labeled state transition system or Kripke structure, we symbolically represent it as BDDs, hence the name symbolic model checker (SMC) [Burch et al., 1990a]. We have to find a way to translate the model into BDDs. Suppose that the current state of the system is represented by a vector of Boolean variables S = {s0, . . . , sn−1} and the next state of the system is represented by a vector of Boolean variables S = {s 0, . . . , s n−1}. Using S and S , the transition relation between the values of the variables in the current and the next states can be stated as a Boolean formula N (s0, . . . , sn−1, s 0, . . . , s n−1). Note a finite-domain non-Boolean variable can be easily converted into a vector of Boolean variables.

Each transition in this transition graph models the passage of one time unit. Without further extensions, non-unit as well as nondeterministic transition time can be modeled by a sequence of unit transitions. It is easy to extend this transition graph into a more powerful model called the timed transition graph (TTG) [Campos et al., 1994].

The symbolic model checker takes as input the model M represented by BDDs and the formula f to be verified (in the initial states of M). For every atomic proposition in S, it outputs a BDD with one Boolean variable such that the BDD is true in a state iff the formula f is true in that state.

CTL can specify the relative ordering of events or actions in a finite state system, but it cannot directly express when these events or actions occur. An awkward way of specifying that some event will occur in the future in at most a fixed number of time units is by nesting EX or AX operators. Real-time systems impose bounds on the response time of events and actions. To handle properties with these quantitative constraints, CTL has been extended in a number of ways. One extension [Emerson et al., 1990] adds time intervals to CTL temporal operators and introduces the bounded until operator U[x, y]. Quantitative algorithms exist for computing the following values between two events: (1) the minimum and maximum delays and

(2) minimum and maximum number of condition occurrences. Also, extensions of these algorithms are available for handling non-unit transition time.

EXERCISES

1.Express the following safety assertion in CTL: In the hospital intensive care unit, once the pulse/blood pressure monitor pad, blood oxygen sensor, and respiration sensor are properly attached to the patient’s arm, index finger, and nose, respectively, and the alarm is enabled, the alarm sounds if any of the following conditions becomes true and remains sounding until a nurse or doctor arrives and disables the alarm: pulse rate is above 120 beats per minute, systolic blood pressure is above 180 mmHg, blood oxygen count is below 80%, or respiration rate is above 35 times per minute.

2.Consider the CES model checker for CTL. If we are going to model the execution of a program with n Boolean variables and m integer variables, each of

132 MODEL CHECKING OF FINITE-STATE SYSTEMS

which ranges from 0 to 10 (inclusive), what is the maximal number of states in the state graph.

3.Consider a simple algorithm for solving the mutual exclusion problem for two processes. Construct the state transition diagram for this algorithm. Prove or disprove the following properties by first expressing them in CTL formulas and then by following as much as possible the labeling technique in the CES model checker.

(a)Only one of the two processes can be in the critical section at any one time.

(b)The two processes will not deadlock.

4.Specify the state graph in exercise 2 as a description for CMU’s symbolic model verifier (SMV).

5.Construct the state graph of the following mobile telephone/entertainment system: While the mobile telephone/entertainment system is turned on, if the telephone subsystem receives an incoming call while the radio, CD, or cassette player is on, then the telephone subsystem will ring after the radio/CD/cassette player is temporarily turned off. The radio/CD/cassette player resumes playing after either: the telephone rings 12 times without a user pressing the “send” button, or the “send” button is pressed within the 12 rings and the conversation is ended by the user pressing the “end” button.

The telephone subsystem does not ring on receiving an incoming call while the mobile telephone/entertainment system is turned off; in this case, the phonemail subsystem is activated to record incoming messages.

6.The goal of this problem is to apply the CES model-checking algorithm to the verification of a timing-based mutual algorithm by Attiya and Lynch, described in detail in [Attiya and Lynch, 1989]. For this problem, assume there are only two operators (processes). Construct the state transition diagram for this algorithm. Prove or disprove the following properties by first expressing them in CTL formulas and then by following as much as possible the labeling technique in [Clarke, Emerson, and Sistla, 1986].

(a)Only one process can be in the critical section at any one time.

(b)The processes will not deadlock.

7.Represent the following Boolean formulas as binary decision diagrams (BDDs):

(a)a (b c).

(b)a (b (c d)).

(c)(a b) (c d).

8.Compare the space requirements for representing a Boolean formula using

(a)a truth table (described in chapter 2) and

(b)a BDD.

9.Explain how the following three types of finite-state graphs together with the temporal logic CTL model transitions with time constraints:

(a)graph with untimed transition,

EXERCISES 133

(b)graph with unit transition time, and

(c)graph with non-unit transition time.

10.Determine the run-time complexity of the minimum and maximum delay algorithms as well as the minimum and maximum condition-counting algorithms.

11.Consider a smart airbag deployment system in an automobile. A sensor is attached to the driver’s seat that detects the distance between the driver and the steering wheel. This distance depends on the shape and size of the driver and on the position of the steering wheel. Based on this distance, the airbag computer determines how fast the airbag should be fully inflated. The airbag will deploy when a collision impact with a speed exceeding 30 mph occurs; otherwise, it will not deploy. If the distance is far (> 1.5 ft), the airbag will be fully deployed within 50 ms. If the distance is average (between 1.0 ft and 1.5 ft), the airbag will be fully deployed within 40 ms. If the distance is near (< 1.0 ft), the airbag will be fully deployed within 30 ms. Specify this system as a timed transition graph (TTG).