P303 Aggarwal

Adding Liveness Properties to Coupled Finite-State Machines S. AGGARWAL and C. COURCOUBETIS AT&T Bell Laboratories and P. WOLPER Universitb de Liege

Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even very simple protocols. Consequently, formal specification methods, such as finite-state models, are increasingly being used. The selection/resolution (S/R) model is a finite-state model with a powerful communication mechanism that makes it easy to describe complex protocols as a collection of simple finite-state machines. A software environment, called SPANNER, has been developed to specify and analyze protocols specified with the S/R model. SPANNER provides the facility to compute the joint behavior of a number of finite-state machines and to check if the “product” machine has inaccessible states, states corresponding to deadlocks, and loops corresponding to livelocks. So far, however, SPANNER has had no facility to systematically deal with liveness conditions. For example, one might wish to specify that, although a communication channel is unreliable, a message will get through if it is sent infinitely often, and to check that the infinite behavior of the protocol viewed as an infinite sequence will always be in some w-regular set (possibly specified in terms of a formula in temporal logic or as an w-automata). In this paper we show that with very minor modifications to the implemented system it is possible to substantially extend the type of properties that can be specified and checked by SPANNER. This is done by extending the S/R model to include acceptance conditions found in automatons on intinite words, which permits the incorporation of arbitrary liveness conditions into the model. We show how these extensions can be easily incorporated into SPANNER (and into essentially any finite-state verification system) and how the resulting system is used to automatically verify the correctness of protocols. Categories and Subject Descriptors: C.2.2 [Computer-Communication Networks]: Network Protocols-protocol verification; D.2.4 [Software Engineering]: Program Verification-correctness proofs; F.3.1 [Logics and Meanings of Programs]: Specifying and Reasoning about Programsmechanical uerification; G.4 [Mathematics of Computing]: Mathematical Software-uerification General Terms: Algorithms, Additional verification

Key Words tools

Verification

and Phrases: Algorithmic

verification,

correctness,

finite-state

machines,

Authors’ addresses: S. Aggarwal and C. Courcoubetis, AT&T Bell Laboratories, Murray Hill, NJ 07974; and P. Wolper, Universiti de Liege, Liege, Belgium. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission. 0 1990 ACM 0164-0925/90/0400-0303 $01.50 ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990, Pages 303-339.

304

’

S. Aggarwal et al.

1. INTRODUCTION Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even a simple protocol, such as the alternating-bit protocol [7 3. This has attracted a lot of attention to formal specification and verification techniques. Among the formal methods for describing protocols [23], finite-state models are one of the most popular. In [5] and [14], a finite-state model with a powerful communication mechanism, the selection/resolution (S/R) model, was proposed. One of the advantages of the S/R model is that its communication mechanism makes it easy to describe complex protocols. Indeed, complicated systems can be described by a collection of rather simple interacting finite-state machines. A software tool for analyzing protocol specifications given in the S/R model, SPANNER, has been developed and is described in [2]-[4]. The main facility provided by SPANNER is the possibility of computing the product machine corresponding to the joint behavior of a number of finite-state machines and the ability to conveniently check properties of this product machine. For instance, one can check if the product machine has inaccessible states, states corresponding to deadlocks of the system, and loops corresponding to livelocks. Even though SPANNER is a successful tool, it shares the usual limitations of finite-state verification systems. For one thing, it provides no facility to systematically deal with liveness conditions. For instance, when analyzing the alternating-bit protocol, it is usual to assume that, although the communication channel is unreliable and might lose some messages, a message will eventually get through if it is sent infinitely often. Such an assumption is essential to the correctness of the protocol; without this assumption it is impossible to establish that any message will ever get through. In addition to this inability for specifying liveness properties of the various components of the specification, the properties (tasks) that SPANNER can prove about the behavior of the system are rather simple; they are directly translated to simple properties of the reachability graph. Powerful formalisms such as temporal logic or w-regular sets cannot be used for specifying tasks in the SPANNER environment. A second limitation of SPANNER is an inability to describe fully and check the overall behavior of a simple data-transfer protocol such as the alternatingbit protocol. This is because the correctness condition we want to verify is that if the transmitter is given an infinite sequence of messages an identical sequence is produced by the receiver. This would involve considering an unbounded number of different messages, clearly an impossibility in a finite-state framework. In this paper we show how SPANNER (or a similar finite-state verification system) can be modified to overcome the two problems we have just mentioned. We show that the necessary modifications to the implemented system are small, and we apply our approach to two examples: Dekker’s algorithm and the alternating-bit protocol. The reason we decided to use these two examples is mainly simplicity; most readers are already familiar with them, which makes it easier to illustrate our specification methodology. A popular formalism for describing the type of liveness condition we are discussing is temporal logic [16, 20, 261. Temporal logic is very different from finite-state machines, but in [25] and [28], it is shown that any set of behaviors A(%¶ ‘hmsactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

l

305

describable in propositional temporal logic is also describable by a finite automaton on infinite words [8, 191. This prompted us to extend the S/R model with the type of acceptance condition found in automata on infinite words. In these automata, one considers the infinite behaviors of the finite automaton (i.e., the infinite sequences of states that are compatible with the transition relation). One then classifies these infinite behaviors as accepting or nonaccepting depending on whether or not they contain some specific states infinitely often. Thus, in our extension of the S/R model, with each finite-state machine component we associate a set of states, at least one of which is required to appear infinitely often in all acceptable behaviors of the machine. As we will show, this makes it easy to distinguish between a communication medium where a message can get lost forever and one where this is not possible. Of course, if we add such an acceptance condition to each of the components of a system, the product machine we compute will have a similar acceptance condition. We can then restrict our analysis to the accepted behaviors of the product machine. To prove a liveness property of the whole system, for example, that some message always eventually gets delivered, it is then sufficient to show that this property holds for all accepted behaviors of the product machine. For this last verification step, we need a formal description of the property to be checked. Our approach is to use a finite-state machine of the sort we have just described specifying the negation of the desired task (property). With this formulation, the system is correct if and only if no accepted behavior of the product machine of the components of the system is accepted by the machine describing the negation of the task, or, equivalently, if the set of the accepting behaviors of the product of the machine describing the system with the machine describing the complement of the task is the empty set. The last step is done naturally within the SPANNER environment as follows: First, we describe the components of the system and the complement of the task in a uniform way as coupled finite-state machines by using the S/R model. Then, we construct the product machine and check if it corresponds to the empty automaton. Note that, with our approach, only minor modification of the finite-state verification system (beyond the addition of accepting sets of states) is necessary to be able to check arbitrary safety and liveness properties of the system. To solve the second problem we have discussed, that is, the inability to specify fully the correctness of a data-transfer protocol in a finite-state model, we turn to the results presented in [27]. There, a method to specify the correctness of a data-transfer protocol in purely finite-state terms is given. The method is based on the observation that the protocols one wants to specify are usually data independent. Basically, a protocol is data independent if the actions it performs do not depend on the specific values of the messages it is transmitting. The result is that if a protocol is data independent its full correctness can be established by showing that it operates correctly on a set of input sequences where only three different types of messages occur. That correctness condition is expressible by a finite-state machine on infinite behaviors, which makes automatic verification possible with no modification of the SPANNER system. With these improvements to the S/R model and the formal specification, we were able to use SPANNER to complete an automatic verification of the ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

306

l

S. Aggarwal et al.

alternating-bit protocol. We also used the same technique on a simpler problemDekker’s algorithm. This is especially interesting as we know of no other techniques that make this possible. The only other complete proofs of the correctness of the alternating-bit protocol are manual and quite tedious [ll, 121. Similarly, the proof of Dekker’s algorithm consists of many pages of formulas [17]. Another interesting aspect is that we were able to do this with a very limited modification of SPANNER and of the description of the alternating-bit protocol. A meaningful anecdote is that our initial verification attempt failed due to a missing liveness condition in the transmitter process. We must emphasize to the reader that, since the facilities originally provided in SPANNER are available in most verification tools based on a coupled finitestate machine model, the method presented in this paper could also be used to enhance the capabilities of any such tool. We chose SPANNER as a convenient vehicle for describing our method and its implementation, but the reader should bear in mind the general applicability of the method. Basically, it is usable in any context in which processes are described by coupled finite-state machines and where the product machine can be computed. However, a broadcasting communication mechanism (such as the one used in the S/R model) makes applying the method used in this paper more natural. Indeed, it makes the addition of new requirements (e.g., liveness restrictions) possible by the addition of components rather than by the redesign of components. This paper is organized as follows: We first review briefly the S/R model and the SPANNER system. Then we turn to finite automatons on infinite words and show how these are incorporated into S/R. We next give a short example (Dekker’s algorithm) illustrating these concepts. We then turn to the alternatingbit protocol, show how its description has to be modified to incorporate liveness conditions, give its full specification based on data independence, and give details of the automatic verification. Finally, we conclude and discuss related work. 2. THE S/R MODEL AND THE SPANNER

SYSTEM

2.1 The S/R Model The S/R model [ 1,3,5,13,14] provides a method of describing a complex system as a set of coordinating finite-state machines. Using S/R, a system is decomposed into a set of simple entities; each entity or process is an edge-labeled directed graph (see Figure 1). The vertices of the graph are states of the process; each directed edge describes a state transition that is possible in one time step. A state is the encapsulation of the past history of the process and is private to that process. In each state, a process can nondeterministically choose from a set of selections (enclosed in braces next to the states in Figure 1). The selections are essentially signals available to all processes for use in coordination. They can be viewed as indicating the “intention” of the process. This broadcasting mechanism used in the S/R model is important for the application of the ideas used in this paper. It makes the additions and deletions of new components relatively simple; the remaining components of the system need not be changed. After all the processes have made their selections, each process decides on a transition to a new state. This resolution is done by calculating the global selection ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

WODUCE(idle,

CONSUME{idle,

write)

I

(X < N) * (P: write)

‘RY(head. tail) (P : done)

l

307

read)

(X > 0) * (C : read)

(C : done)

I

(P: idle, write, done) + (P : head) t (C : tail) + (P : tail) * (C : head)

(C : idle, read, done) + (P : head) * (C : head) + (P : tail) * (C : tail)

48 (writing, done}.

ABfreading,

CONSUMER

PRODUCER (P)

*o .

(c : done)

0

(P: done)

lOI

1

Ill

(P:done)

2

e

done)

(C)

N + 1 {error)

(P:done)

(P: done)

121

N

IV

BUFFER (X)

Fig. 1. Example selection/resolution

description.

(the product, i.e., the Boolean AND, of all the current selections of the processes) and then determining the edges that are possible transitions. Edges are labeled by elements of a Boolean algebra generated by the selections of the processes. We calculate the product of each edge label out of the current state with the global selection to determine if it is 0 or not. If the product is 0, the transition is not enabled. Informally, each process checks to see which transitions are consistent with the current selections of all processes and then chooses one of these enabled transitions. Consider the case of k processes PI, . . . , Pk, and let the selection of Pi be si at time step t. Then the global selection s = slsz . . . sk is the AND (in the Boolean algebra) of the individual selections. If process Pi is in state u at time step t, and the label on the edge from u to w is F, then w is a possible state at time t + 1 if s . / # 0. It is important to note that each process resolves independently, using the common global selection. Also, note that the edge conditions incorporate any interaction of the processes. ACM Transactions on Programming Languages and Systems, Vol. 12, No. 2, April 1990.

308

l

S. Aggatwal et al.

2.2 The Process Let L be a Boolean algebra in which AND is denoted by . (product), OR is denoted by + (sum), and NOT is denoted by - (negation). An L-process P (or process, for short) is a 5-tuple p = (VP s, c, M, 0, where (1) (2) (3) (4) (5)

V is the set of states of P; S is the set of selections of P, S C L; u is the selector function of P, u: V += 2’ ; M is the transition matrix of P, M: V X V + L; and I is the initial state of P, I E V.

(1)

The selector function associates with each state u the set of possible selections a(v) that can be made from state u. The transition matrix can be viewed as an adjacency matrix of a directed graph with vertices V where the nonzero entries are actual labels describing the conditions for a transition to be enabled. Given an edge label / = M(u, w) from state u to w, if the selection of the process is s in state u, then s . / # 0 means the transition to w is possible. 2.3 The Composition

of Processes

An important feature of the S/R model is that one can define a “calculus” on the processes so that the “product” of processes is again a process. Intuitively, the product process corresponds to the joint execution of the component processes. The product process is naturally viewed as a graph that is the product graph of the individual processes. This product is termed the tensor product 63, since the transition matrix of the product process is the tensor product of the transition matrices of the component processes. Let 8 denote the tensor product of matrices; that is, (A 63 B)(;,j),(k,/) = A(i,k) * B(j,/), where * is the product operator in the Boolean algebra L. Given processes PI, . . . , P,,, with Pi = (Vi, Si, ai, Mi, Ii), we define their product P = @rzl Pi to be the process P = (V, S, u, M, I), where (1) V = Xyi=, Vi---an element (ul, . . . , u,) E V is also denoted by BY=1 Ui for convenience (X denotes the Cartesian product); (2) S = nyZ1 S’i-n denotes the product of sets of labels (or functions into labels) as usual, that is, for C, D, E 2L, let C . D = (cd 1c E C, d E D]; (3) UC n&Ui; (4) M = a?==,Mi; and (5) I = (I,, . . . , I,). (2) 2.4 Assumptions

on the Boolean Algebra

In this paper, and in the SPANNER software, there are two assumptions made on the Boolean algebra L of selections and labels. We assume that the algebra is generated by the selections of the processes, modulo the relations imposed by assuming that two distinct selections of a single process cannot be made ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines simultaneously.

Thus, we assume that

(1) for distinct

selections (Pi : X) and (Pi : y) of process Pi, (Pi:X)

’ (Pi:y)

l

309

= 0;

and (2) for processes Pi, . . . , P,, and selections (Pi : si),

These assumptions give rise to a standard labeling format without the types of coordination that can be modeled [6].

restricting

2.5 Chains and Process Behaviors The S/R model is a discrete time model in which the states and selections of a process are defined at the nonnegative integers. Suppose the process at time step k is in state u = u(k), choosing a selection s = s(k) with s E a(u). Then, at time step k + 1, we can determine the state u’ = u(k + 1) and selection s’ = s(k + 1) as follows: We evaluate s . M(u, w ) for all w E V. Let the possible next states N(u, s) = {w ] s . M(u, w) # 0, w E VI. We choose some element u’ E N(u, s) as the next state. If there is more than one next state in N(u, s), the choice is arbitrary. If N(u, s) is empty, our labeling is faulty, and we have a condition known as lockup with no next state defined and no future behavior possible. Lockup should not be confused with deadlock; deadlock in our model occurs in a state u if, for all available selections s at that state, N(u, s) = fu). After determining a next state, the process determines a new selection s’ E a(u ’ ). Again, we have a nondeterministic choice of selections possible if there is more than one selection available in state u’. A chain of a process is a sequence of state-selection pairs consistent with the dynamics described above. Intuitively, a chain is a sample path of the behavior or possible history of the process, where at each time step we record the state and the selection of the process. Formally, a chain is c = (c(O), c(l), where the following

* * * ),

hold:

(1) c(k) = (u(k), s(k)), where u(k) E Vand s(k) E a(u(k)) for all k. (2) u(O) = I, the initial state. (3) u(k + 1) E N(u(k), s(k)) for k ~0, unless N(u(k), s(k)) is empty, in which case the chain terminates. The set C of all chains of a process thus represents all possible behaviors of the process. So far, we have focused on the behavior of a single process P. Given processes PI, ***, P,, one way of defining the behavior of the processes jointly (possible sample paths) is simply to define the chains of P = @?=I Pi and then take projections to determine the component process chains. This is the synchronous product. We can model asynchronous processes as well by adding a selection ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

310

l

S. Aggarwal et al.

’

Formal specification

Parser

Reachable graph

Simulation

‘-1

Analysis Fig. 2.

SPANNER

1

environment.

called “pause” selection and providing the corresponding labeling; see the example in Section 4. Equivalently, we can first define the global selection s = s(k) = sl(k) . sz(k) . . . s,(k) of the n processes, where process Pi is in state u;(k) at time step k. Then, a possible next state Ui(k + 1) of process Pi is determined by considering Ni(Vi, S) = (wils * M~(IJ~, WI) # 0, Wi E Vi] and choosing an element u&! E IVi. This corresponds to multiplying each edge label ! out of state ui by the global selection s and checking ifs. Y # 0. A global next state is (vi, u;, . . . , u;) with u( E Ni(ui, s). We generally take this latter approach when describing the chains of a set of processes. 2.6 Overview of the SPANNER System SPANNER (2-41 is an environment consisting of a set of modules (see Figure 2) for specifying and analyzing protocols. A user would first formally specify a protocol using the SPANNER specification language. The parser module checks this specification for syntactic correctness and produces an intermediate description used by other modules. Next, the user has two choices. One option is to generate a database consisting of all global states reachable from the initial state. The second option is to produce a database consisting of a sample of the reachable states obtained by doing a simulation run. This is particularly useful for very complex protocols, since interesting constraints can be imposed on the simulation. For example, it is possible to assign probabilities to the selection choices, and it is also possible to force a selection to be held for a particular number of time steps [2]. ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines constants

l

311

N = 3

process P /* the producer */ import C, X states 0..2 valnm [PRODUCE : 0, AB : 1, TRY : 21 selections 0..5 valnm [idle : 0,write : 1,writing: 2,done: 3,head: 4, tail : 51 init PRODUCE trans PRODUCE (idle,write] > TRY :(X < N) * (P : write); :otherwise; =-$ TRY >AB >$

(head,tail] :(C : idle,read,done) :otherwise;

AB > PRODUCE >$

(writing,done] :(P:done); :otherwise;

+ (P : head) * (C : head) + (P : tail) * (C: tail);

end process C /* the consumer */ import P, X states 0..2 valnm [CONSUME: 0, AB: 1, TRY: 21 selections 0..5 valnm [idle : 0,read: 1,reading: 2,done : 3,head: 4,tail: 51 init CONSUME trans CONSUME {idle,read] > TRY :(X > 0) * (C:read); :otherwise; >$ TRY >. AB >$

{head,tail 1 :(P: idle,write,done) :otherwise;

AB > CONSUME =-$

(reading,done] :(C:done); :otherwise;

+ (P: head) * (C : tail) + (P: tail) * (C: head);

end process X /* the counter */ import P, C states O..N + 1 valnm [ERROR: N + l] selections O..N + 1 valnm [error: N + l] init 0 trans $ ISI > ($ + l)%(N + 2) :(P:done); > ($ - l)%)N + 2) :(C:done); :otherwise; >$ end Fig. 3.

SPANNER

specification

of the protocol

of Figure 1.

Finally, the user can analyze the results of the reachability (or the simulation) by querying the generated database using an interactive query language. The querying would determine whether certain global states are reachable, if there are any deadlocks, and other properties of interest. The basic entity of the specification language is a process; this corresponds to an S/R process as defined in Section 2.2. Figure 3 shows the processes described ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

312

l

S. Aggarwal et al.

by the graphs of Figure 1 in the SPANNER specification language. The initial declaration of a process simply describes the ranges of its states and selections and gives the user the option (using the keyword valnm) of providing descriptive names for these states and selections. The import declaration is used to force the user to declare the external selections that will be used in that process. The init declaration declares the initial state of that process. The trans section consists of blocks that describe transitions from a state to its next states. (Current state can also be a set of states if all the transitions are identical.) The format of a block is as follows: current state next state ... ... > next state >

(selection list) :condition;

:condition;

A cluster is a grouping of processes or other clusters. Clusters are useful in hierarchical descriptions. A selection(s) of a cluster is derived from the selections of its “children” and is specified by a mapping function. The specification language supports a variety of useful constructs [3]. In the specification language, we use the shorthand $ to mean the current state, and we use (P.$ : Vi) to represent a predicate that is true when the state of P is equal to vi. We use the keyword otherwise to indicate the negation of the or of the previous conditions in a block. In the language, we use * or & for product, and we use + or ] for sum. These features will become clearer as we go through the examples. 3. ADDING

LIVENESS

PROPERTIES

3.1 Processes with Acceptance

Conditions

Consider the case of a channel that delays a message for some arbitrary but finite time before delivering it. It is clear that a process defined as in Section 2.2 cannot model such a device accurately, since by allowing it to keep the message for an arbitrary length of time, we must also allow it to keep the message forever. Such “liveness” properties can only be expressed if one makes the model more powerful. We do this by adding acceptance conditions to our basic process. Our formulation is related to the theory of automata over infinite words [8, 191. Definition.

An L,-process P is a 6-tuple P = ( K S, u, M, I, F),

where (1) V, S, (r, M, and I are defined as in (2); (2) F = (F,, . . . , F,,,), Fi C V, i = 1, . . . , m, is a set of accepting sets of states; and (3) a chain c of P is accepted iff it repeats some state from each Fi infinitely often. (3) ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

*

313

(CH: done)

KH : store) (CH: deliver)

DELAY (store,

deliver}

F = {DELIVERED) PROCESS CH (CHANNEL) Fig. 4.

Definition

of the channel process.

Our acceptance condition is more general than the one proposed by Biichi [a], where m is always 1. However, it can be shown that our acceptance condition has the same expressive power as the one proposed by Biichi in the sense that, for any &,-process, one can construct a I,,-process with a Biichi acceptance condition that accepts the same set of chains. We use this more general type of condition as it is more convenient for our purposes. As an example, in Figure 4 we use the above definition to model the channel example mentioned in the introduction. The accepted chains are of the form’ u*bcw, where a = (DELAY, store), b = (DELAY, deliver), and c = (DELIVERED, done). Note that without the acceptance condition nothing would prevent the process from staying forever in the state DELAY. As in the channel example, we follow the convention of writing F = Fl rather than F = (F1) whenever F contains only a single set. Thus, we wrote F = (DELIVERED] rather than F = ((DELIVERED]). Also, if F = Fl and Fl consist of all states of the Process P, that is, if F = V, then it should be clear that an Lo-process accepts all chains c E C and is equivalent to an L-process. In such a case, we do not explicitly write the set F. We can easily derive the acceptance condition for a product of processes in terms of the acceptance conditions of the component processes. A chain of the product process is accepted iff its projection onto each individual process is accepted by that process. For example, let PI have states VI and acceptance conditions Fl = (Fll, F12), and P2 have V, and F2 = (F,, ). Then the acceptance condition F of P = PI 8 Pz is F = (F,, X V,, F,, X V2, V, X F,, ).

3.2

Monitor

Processes

Since the behavior of a process is given in terms of its accepted chains, it becomes of interest to determine whether the chains of the process satisfy some given properties. In many applications, these properties are called the tusiz to be accomplished by that process. One way for specifying a task is to give a process that observes, but does not participate in, the execution of the concurrent system. We call such a process a monitor. Abstractly, one can think of a monitor as an automaton on infinite words, whose input alphabet consists of all possible stateselection pairs of the monitored process. 1 We use * to denote finite repetition, expressions and w-regular expressions. ACM Transactions

and w to denote infinite on Programming

repetition,

as is done in regular

Languages and Systems, Vol. 12, No. 2, April 1990.

314

l

S. Aggatwal et al.

A monitor is exactly like an L,-process in (3), with the only differences being that (1) the monitor process’s selections are not used by other processes (since it only observes) and (2) a transition of the monitor process can be labeled with a Boolean expression on selections and states of the monitored processes (instead of just selections). Monitors can also be used to describe constraints on process behavior. Since we can build a monitor process M to accept a given subset of the chains produced by a process P, it follows that P ’ = P 0 M corresponds to the constrained process P with the constraints described by M. It is possible to construct such monitors algorithmically if the specification of the set of chains the monitor should accept is described by a formula in temporal logic. This could be done by using the algorithms in [28] to construct the Biichi automaton corresponding to the above formula. The alphabet of this automaton would consist of the (global-state, global-selection) pairs of the product of the components of the specification. Interestingly, the converse construction is also possible if one uses the extended temporal logic (ETL) of [25] and [28]. Indeed, it is shown there that ETL can express any property describable by a Biichi automaton and, consequently, any set of chains specified by an S/R monitor process. Thus, S/R processes with acceptance conditions and ETL are expressively equivalent. Note that the algorithms described in [28] are in practice unusable as such. They can be improved and made more practical, but would always be limited to short formulas since their behavior is intrinsically exponential. 3.3 Proving Correctness We now give a formal description of our approach for proving correctness. The formal specification of the protocol P consists of a set of component processes PI, a**, P,, where each Pi is an L,-process or a monitor process corresponding to some desired constraints. Thus, the protocol is P = @~zlPi. A task T, defining a desired set of chains that should be accepted by P, can also be represented by a monitor process. However, it is more convenient for us to consider the complement of the set of desired chains, and thus, we describe the negation of the task to be accomplished by the protocol as a monitor process TC. We can now reduce the problem of proving the correctness of the protocol to the problem of checking for the emptiness (no chains accepted) of the product process P ’ = P 0 TC. Indeed, if P’ has no accepting chain, it follows that there is no chain accepted by P, that is, produced by the protocol, that is also accepted by TC, that is, that contradicts the task. Checking for the emptiness of P’ is straightforward using SPANNER. The check is based on the strongly connected components of the reachability graph of P’. We distinguish between two types of strongly connected components: (1) A transient strongly connected component has only one state, and there is no transition from that state to itself; and (2) a non-transient strongly connected component is any other strongly connected component (see Figure 5). We thus check if there exists a nontransient strongly connected component Q C V’ for which Q fl Fc # 0, for all i = 1, . . . , m. (V’ and (Fc ) are the set of states of P ’ and the acceptance sets of P ‘, respectively.) If there is no such strongly connected ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

l

315

8 4

5

A REACHABLE GRAPH (INITIAL STATE IS 1)

STRONGLY CONNECTED COMPONENTS: {1}, {2,3,4,5},

{6},{7,8}.

TRANSIENT STRONGLY CONNECTED COMPONENTS: (6). NONTRANSIENT STRONGLY CONNECTED COMPONENTSI {I}, {2,3,4,5,},{7,8} Fig. 5.

Strongly

connected components.

component, then the accepting conditions of P’, including those of the task complement TC, cannot all be satisfied, and hence, P ’ = P 8 TC accepts only the empty set. By implementing an algorithm that computes the strongly connected components of a graph in linear time in the size of the graph, the above verification step is done in time linear in the size of the complete specification, that is, the size of P’. Interestingly, this algorithm (based on depth-first search) was already implemented in SPANNER, and the information about connected components was available in the representation of the global-state machine generated by SPANNER. So, to adapt SPANNER to the type of verification we are interested in, we only had to improve the exploitation of the database representing the global-state machine. It should also be pointed out that a task T might itself be represented as T = T, @ T2 GO. . . C3 Tk. In this case, we can independently check if P 8 TCi is empty for i = 1, . , . , k. This is more efficient than checking for the emptiness of P C3 TC, since it reduces the size of the sets of global states that must be constructed. Furthermore, constructing each TCi is much easier than constructing TC. 4. DEKKER’S

ALGORITHM

We now illustrate our method by using it to prove the correctness of a well-known parallel algorithm of the literature: Dekker’s algorithm for mutual exclusion. We repeat here the description of the algorithm as found in [17]. There are two parallel processes PI and Pz, a shared variable t that may be modified by both processes, and two private Boolean variables y, and yz. Each private variable may be set only by the process owning it, but may be examined by both. The parallel program is shown in Figure 6. ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

t:=l,

yl:=yz:=F

Program PI

Program P2

e.0.

execute

mo:

execute

e,:

y, := T

ml:

y2:=

T

t,:

if ti2 = F) then go to e,

ml:

if69

= F) then go to m7

e,:

if(r=

mj:

if (I = 2) then go to ml

e,:

y1 := F

m4:

y2 := F

loop until (r = 1)

m5:

loop until (t = 2)

e,:

go to e,

me:

gotom,

e,:

g0

e,

m9:

go to mo

t0

l)thengoto&

Fig. 6. Dekker’s algorithm.

(P, : pause) + (P, : execute)

(P, : check)

(t : 1) (yl:T)

(PI :check)

(P, : pause)

(P, : pause) + (P, : check) . T(t : 1) PROCESS P, (Pa IS SYMMETRICALLY

DEFINED)

(a)

Fig. 7. Specification of Dekker’s algorithm.

Adding

Liveness

Properties

to Coupled

(P, : y4 :=T)

Machines

l

317

(P2 : yp: = T)

(P,l

y2:=T)

(P4 * y4:‘F)

PROCESS

Finite-State

YI

(P2’ y2’=

F)

PROCESS

y2

(P 4 :t~.2)+‘(P2:t’=l) PROCESS

t

04 Fig. 7.

(Continued).

The variable y1 in P, (y2 in P2) is set to Tat Ll to signal the intention of P, to enter its critical section at e7. Next, PI tests at P, if P2 has any interest in entering its own critical section by checking if y2 = T. If y2 = F, PI proceeds immediately to its critical section. If y2 = T, there is a competition among the two processes on the access right to their critical section. This competition is resolved by using the “turn” variable t whose value indicates the process that should win the conflict. If t = 2, then PI “drops out” by setting y1 to F and waits ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

318

S. Aggatwal et al.

l

until its turn comes (t = 1). If t = 1, it waits until Pz “drops out” and then enters its critical section at Y7. While in the critical section, it sets the turn variable to 2, to indicate that next time a potential conflict should be resolved in favor of Pz, and sets y1 to F just before exiting the critical section. We assume that P, and Pz are running asynchronously on different processors with different speeds, and that read and assignment instructions involving shared variables are executed as atomic operations. The above parallel program is correct if it satisfies the following two tasks: T,: T,: T,’ :

never (at (Y,, e8) A at (m7, m,)) (safety), at J’, implies eventually at r7 (liveness), and at lTtl implies eventually at m7 (liveness).

Since PI and P, are symmetrically defined, it is sufficient to prove T2 instead of both T2 and T,‘. In order to prove the correctness of Dekker’s algorithm, we proceed as follows: We model the processes Step A: Formal specification of the parallel program. P, and Pz as well as the variables yi, y2, and t as coupled finite-state machines by using the ideas introduced in Section 2. The corresponding processes are shown in Figure 7, and their specification using the SPANNER specification language is in Appendix A. Processes PI and P2 are systematically derived from their corresponding program by associating a state to each instruction (es and f9 are encoded as transitions) as follows: A state has two selections, the pause selection and the selection corresponding to the execution of the instruction corresponding to that state. The labels of the processes are such that when a process selects to pause it always stays in the same state irrespective of the selections of the other processes. If a process selects to execute an instruction, then it transitions to a state corresponding to the instruction of the program that would be executed next after the previous instruction would be executed by the above program. The pause selection enables us to model the asynchrony of the processes. While selecting pause, the process must remain in the same state independently of the other processes in the system. Variables are modeled by processes having as many states as the variable can have values. In each state, the only possible selection is the corresponding value of the variable. There is a transition for each possible assignment to the variable. The atomicity of the assignment operations to the variable t is modeled as follows: If both PI and P, attempt to assign a value to t simultaneously, then t will nondeterministically choose one of the two values as its next value, corresponding to some arbitrary serialization of the two assignment operations. We note that this initial specification is not complete. Nothing precludes an execution of the processes in which a process pauses forever from some point on. However, this is not in agreement with our interpretation of the parallelism of the processes, which is that each process P, and P2 will always eventually execute its next instruction. We eliminate these unacceptable executions by introducing two additional monitor processes LC, and LC,. LCi monitors Pi and accepts only these infinite paths on which Pi does not eventually always pause. These processes thus model our desired liveness conditions. The processes are shown in Figure 8 ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

.

319

(Pi : pause)

(Pi : pause)

(Pi: pause) Fig. 8. rithm.

Liveness

conditions

for

Dekker’s

7 (pi: pause)

PROCESS LCi , i = 1.2

and are also shown in the SPANNER specification Note that their set of accepting states is F = (1). The specification of the parallel program is thus

language in Appendix

A.

Step B: Formal specification of the task. The task to be accomplished by the parallel program is described in terms of the conjunction of the two conditions Tl and T2. Recall that to check that P satisfies the conjunction of Tl and T2 it suffices to independently check that P satisfies T, and P satisfies Tz. Now, to apply our method for proving that P satisfies T1 and T2, construct the negations of Tl and T2 as automata on infinite words. These automata, described as monitor processes, will track the chains of the specification processes and will accept all chains that do not satisfy the task. It is straightforward to construct these automata and the corresponding monitor processes as illustrated in Figure 9. (TC, and TC, correspond to the processes accepting the complement of T, and T2, respectively.) Building the S/R process describing the complement of the task is often easy, but can be hard if the task is complicated. One solution to this problem is to describe the task in propositional temporal logic [20, 261. Temporal logic is generally considered as a convenient language for describing properties of infinite sequences, especially liveness properties. Also, given the results in [28], it is possible to algorithmically build an S/R process whose infinite chains are exactly those satisfying a given propositional temporal logic formula. One could thus describe the task by a propositional temporal logic formula, build the S/R process corresponding to the negation of that formula, and then use the verification ACM Transactions on Programming Languages and Systems, Vol. 12, No. 2, April 1990.

320

l

S. Aggarwal et al.

1

((P,.$: 4,)+(P,.$:+J)

-

((P2.$:m7)t(p2.$:mg)) 2 >

0 F = 121

PROCESS TC, Fig. 9.

Task complements

for Dekker’s

algorithm.

1 (P,.$ : 4,)

f =01 PROCESS TC2

method we have just described. We have not, at this point, implemented the translation from temporal logic to S/R processes, but we believe it could be a very interesting addition to the SPANNER system. Step C: The proof of correctness. To prove the correctness of Dekker’s algorithm, we need to check for the emptiness of P @ TCi, i = 1, 2. This was successfully done using SPANNER, following the procedure described in Section 3.3. Both P 8 TC1 and P @ TC2 were empty. It is interesting to compare the small amount of simple work involved in the use of our method to the multipage proof of the same algorithm in [17]. Furthermore, our approach is completely mechanical, whereas the proof in [17] demands a substantial degree of ingenuity. 5. THE ALTERNATING-BIT

PROTOCOL

In this section we show how SPANNER can be used to give a complete proof of the alternating-bit protocol. We first give an overview of the protocol and then discuss the addition of the liveness conditions to the specification. Next, we ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

l

321

discuss the task that is required to be performed by the protocol, and finally, we show that the specification satisfies the task. 5.1 The Protocol

Our description of the alternating-bit protocol is similar to the description that we have given in previous papers [3, 51. This description is more complete than that usually found in the literature and captures many important features of more complex protocols. The protocol is designed to ensure that messagesare delivered in order, from a sender to a receiver, in the presence of channels that can possibly lose messages. We first model the upper layers consisting of the sender and the receiver that simply generate and receive messages, respectively. We model the (lower layer) channels as two clusters called the incoming channel and the outgoing channel. The peer-level protocol is modeled as a sending cluster and a receiving cluster that implements the mechanics of the protocol. Each of these clusters consists of several processes, as shown in Figure 10. The formal specification is given in Appendix B and can be better understood after reading Section 5 completely. Note that we require the sender to generate only three different types of messages. This is discussed further in Section 5.3. The sending protocol works as follows: Get a message from the sender if the sender wishes to send a message. Send the messagetogether with a bit of 0 or 1, and set a timer. Wait for an acknowledgment that the messagehas been received correctly, and if so, send the next message. If an incorrect acknowledgment is received, ignore it. If the timer times out, resend the same message.The receiving protocol always acknowledges the bit (0 or 1) of the last correct messagereceived. It gives a single copy of the message to the receiver and discards any duplicate messages. 5.2 Adding Liveness Conditions

Our method of introducing liveness conditions is by defining (one or more) sets of accepting sets for processes of interest. For example, in the alternating-bit protocol, for the timer process TI, the accepting set is defined to be (OFF, TO). See the comment in the process specification of TI in Appendix B. This forces the timer to eventually always leave the ON state and thus is equivalent to saying that the timer once set will always time out. In our initial description, we did not have an accepting set for the transmitter process TR, allowing it to forever be sending an “infinitely long” message. In our proof, discussed in Section 5.4, this error was located, and we then added the accepting set (READY, WAITING}. This forces the process TR to eventually always leave the state TRANS, which corresponds to the termination of transmission of the message. Sometimes it is easier to add a monitor process and accepting conditions on that process, in order to ensure a liveness condition. This was what we did in order to ensure the desired liveness conditions for the channels in the alternatingbit protocol. Informally, our condition was that, if the channel is given a message infinitely often, eventually it delivers the message. Thus, the channels should not forever lose the messages.The basic description of each channel consists of two processes that keep track of the message type and sequence number. For ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

‘

layer

,

i Upper I

Sending protocol cluster SP

Fig. 10.

I

I I

I I

I I I

I I

I

I

I I I

I

Alternating-bit

protocol.

Lower layer

Incoming channel cluster CHI

Outgoing channel cluster CHO

I

-L

I I I

I I I I

I I I

I I Receiving protocol cluster RP

I

layer

Receiver R

: Upper

I I I I

I I I I I I I I I

I I I I

Message analyzer MA

I I I

I

I I I I I I I

I I

I I I I

I I I

I I

I I I I I I I

I I I I I I I

Adding Liveness Properties to Coupled Finite-State Machines

l

323

example, the outgoing channel cluster consists of process M and process SN. Process M models delivery or loss of the message. Since delivery or loss is determined by a selection of the process, however, it was not possible to add the liveness condition to the processes as defined. (Of course, the original description could have been modified.) Instead, we added the liveness condition by constructing a monitor process CHOLC consisting of five states and by requiring that the accepting set be {NORMAL, LOSTMOK). This corresponds to two conditions. The first condition is that the monitor eventually always returns to the NORMAL state, meaning that the message is delivered, and that the channel is no longer holding or losing the message. The second condition that is acceptable is that the channel loses some messages; however, the transmitter never subsequently gives the channel another message. This is represented by the state LOSTMOK that is also an accepting state. Figure 11 graphically describes this monitor process; the only infinite sequences that are allowed are those that (can) go through NORMAL or LOSTMOK infinitely often. Notice that there is nondeterminism out of state GETM since the loss selection can lead to either state LOSTMOK or state LOSTMNOK. The notion of acceptance of a sequence is the nondeterministic automata notion; that is, for some appropriate choice of transitions, the sequence can be accepted. The liveness condition of the incoming channel is modeled similarly to the liveness condition of the outgoing channel and consists of a monitor process CHILC with the accepting set (NORMAL, LOSTMOK].

5.3 Specifying the Task In simple terms, the correctness condition for a data-transfer protocol, like the alternating-bit protocol, is that the sequence of messages received be identical to the sequence of messages sent. To be precise, let us view our protocol as a black box with one input and one output. Let us assume that the messages given to the inputarem,,mz,,.., where the rni (i L 1) are all distinct. We want to specify that the sequence of messages produced at the output is identical. This can be done with the following conditions: (1) For all i, if (and only if) the message mi is read at the input, then eventually it is produced at the output, and it is produced only once. (2) For all i, j, if the message mi precedes the message mj while being read by the input, then mi precedes mj in the output. The problem with these requirements is that they involve an infinite number of different messages. This makes it impossible to describe them as (finite-state) S/R processes. If our protocol has a behavior independent of the values of the messages, however, then the property can be stated using finite-state processes. A precise definition of data-independent protocols can be found in [27]. A sufficient condition for a protocol described in S/R to be data independent is that everywhere in the protocol the transitions are independent of the value of the message being transmitted. An inspection of our S/R description of the alternating-bit protocol shows that it satisfies this condition. ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

324

-

S. Aggatwal et al.

nodata

pause deliver I

0

nodata F = (NORMAL, Fig. 11.

Informal

description

LOSTMOK)

of channel liveness conditions.

Given the data-independence property, it can be shown that it is sufficient to use three different message values to establish that properties (1) and (2) above hold on any sequence of distinct messages. Specifically, it can be shown that, given data independence, if whenever the sequence of input messages is of the form rn? m2 rn? m3 ml, that the sequence of output messages is of the same form, then conditions (1) and (2) above are guaranteed to be satisfied. The idea is that because the protocol is data independent, if it fails to transmit a message or inverts two messages, this can be detected by a sequence of the given form. More details about data independence and a precise proof of the result we are using can be found in [27]. In terms of verifying the alternating-bit protocol, this result implies that if the input to the protocol is provided by the sender process described in Figure 12 then it should satisfy the task described in Figure 13. Hence, to verify the correctness of the alternating-bit protocol, we take the composition of the description of the protocol, including the process S of Figure 12, and the process given in Figure 14, which is exactly the negation of the task given in Figure 13. This monitor process, TC (task complement), is included in the formal specification in Appendix B. To intuitively understand the description of the complement of the task in Figure 14, observe that the task is not satisfied either if the ACM Transactions on Programming Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines wait

wait

idle

wait

l

325

wait

idle

wait

idle

s, A (S:l) S? P (S:2) s.3 n (S:3) idle done wait

n (S : idle) a (SP.tosender : done) L (SP.tosender: wait)

Note: Selection sets not shown; see Appendix 8. F= ION11

Fig. 12.

(R:pause,

1)

(R:pause,

Sender process.

1)

(R : pause)

F = {d)

Fig. 13.

Task for the alternating-bit

protocol.

sequencing of the messages is wrong (in which case one would reach the state “error” and stay there forever) or if after some point the expected next message is not received (which corresponds to staying in state “a,” “b,” or “d ” forever). 5.4 The Proof

The task to be proved was that messages were received in the order sent, under the conditions imposed by the liveness conditions of the protocol. As discussed ACM Transactions on Programming Languages and Systems, Vol. 12, No. 2, April 1990.

326

S. Aggatwal et al.

l

(R: pause, 1) (R : pause, 1)

F= {a,b,d, Fig. 14.

Complement

(R : pause, 1)

(R: pause)

error}

of the task for the alternating-bit

protocol.

in the previous section, the complement of the task was represented by the process TC with the accepting set (a, b, d, error). Any infinite sequence that satisfies this accepting set is an undesirable sequence. In our first attempt, we used SPANNER to check the consistency of the task complement with the following accepting sets: s:

(ON11 (OFF, TO]

%LC:

(NORMAL, (NORMAL,

CHILC : TC:

LOSTMOK) LOSTMOK)

(a, b, d, error)

To our surprise, we discovered that there was a nontransient strongly connected component for which all the conditions were satisfied. Upon inspection of the states of the processes in one of these components, we found that the transmitter was always in the ON state. We realized that our specification allowed the transmitter to be always transmitting, and thus, the task could not be satisfied. We next added the accepting condition that forces the transmitter to eventually terminate sending the message: TR:

(READY,

WAITING}

Upon rechecking with this additional constraint, we discovered that there was no longer any nontransient strongly connected component that could simultaneously satisfy all the conditions. Thus, the task was proved. 6. CONCLUSIONS

AND RELATED

WORK

The goal of this paper was to show by example that a few ideas can significantly extend the type of properties that can be checked by finite-state verification systems. The first such idea is to use acceptance conditions similar to the ones ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

l

327

used in finite automatons on infinite words to model liveness conditions. The second is to specify the property to be verified by a finite-state machine accepting the complement of the desired behaviors. The third is to use data independence to specify data-transfer protocols. One interesting point is that these ideas require very little modification of a classical finite-state verification system in order to be usable. This makes it possible to benefit fully from the years of work that have often been put into the development of such systems. We applied them to the SPANNER tool, which is based on the S/R model, and with almost no change to the implemented system, we were able to give a fully automatic verification of Dekker’s algorithm and of the alternating-bit protocol. A similar result can probably be achieved with other finite-state verification systems. One element that was helpful in SPANNER is that the communication mechanism between processes has a broadcast nature and hence can be used to synchronize any number ‘of processes on a given event. This makes it easy to modify and extend specifications by adding components rather than by redesigning components. A first sketch of the ideas of using finite automatons on infinite words and data independence for extending the use of finite-state verification appeared in [22] and in the essentially identical [21]. The method presented there was preliminary, had some drawbacks, and was not based on an existing implemented system. First, a nonbroadcast communication mechanism was used. This made it impossible to separate the liveness and safety part of the specification of a process. Only one finite-state machine could be used for each process, which led to quite complex machines. Furthermore, the composition of processes was not well defined. In particular, there was no clear model of parallel composition as defined in S/R. It was also proposed that this machine could be automatically generated from a temporal logic specification. This is indeed theoretically possible, but requires a substantial amount of work to be put in practice. Here, we preferred to exploit the flexibility of the S/R model for combining processes and to give the liveness condition directly as a finite-state machine, which is usually quite easy. Second, in 1221 the verification was partly done by a reduction technique. This worked well in the case of the alternating-bit protocol, but was not extended to a general framework. Moreover, it requires new algorithms, whereas our method does not require modifying existing finite-state verification systems. A related approach to deal with liveness conditions is being developed by R. P. Kurshan (personal communication, 1986). There, liveness conditions are imposed on arcs rather than on states. The idea of data independence was first mentioned in [22] and put on firm ground in [27]. Here, our point is to show that it can be very easily and profitably exploited in the context of a finite-state system when it is combined with the other ideas mentioned in this paper. The approach we have described in this paper naturally brings to mind “model checking” [9, 15, 241. In fact, as one can see from the procedure outlined in [24], model checking for linear-time temporal logic is essentially the procedure used in this paper, but where the task is first described as a temporal logic formula and then converted to a Biichi automaton. The point we have made here is that one can avoid this last step, and given this, model checking is something that can be done with existing finite-state verification systems. This is pragmatically ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

328

S. Aggarwal et al.

l

quite important. Model checking was actually first defined in the context of branching-time temporal logic [9, lo]. In this approach one still computes the global-state machine, but then uses a special-purpose algorithm to check that this machine satisfies properties expressed in branching-time temporal logic. In [lo] this algorithm is applied to the alternating-bit protocol, but no complete verification of that protocol is given. This is in part because the idea of data independence was not used. It is conceivably possible to adapt it to this framework, though it fits more naturally in a linear-time context. The only other proofs we know of Dekker’s algorithm or of the alternating-bit protocol are manual and use first-order logic or a first-order version of temporal logic [12, 161. It is conceivable that these proofs could be restricted to a propositional version of temporal logic and hence automated using the decision procedure for that logic. However, this would require a good implementation of this decision procedure, which is a nontrivial task. Moreover, a close analysis shows that such a decision procedure has a fair amount of similarity to the process of combining finite-state automata and checking for their emptiness. We thus prefer our approach, where we can do this construction within an existing system.

APPENDIX process

A. FORMAL

Pl

import y2, t states 0..7 selections 0..5 init 10 trans 10 >ll =-$

SPECIFICATION

valnm valnm

(pause,execute) :(Pl : execute); :(Pl : pause,execute); (wuse,yleG”) :(Pl : yleqT); :(Pl:pause);

12 >17 >13 >$

(pause,check) :(y2 : F) * (Pl : check); ‘“(~2 : F) * (Pl : check); I(P1: pause);

>12 >14 >$

(pause,check) :(t:l) * (Pl:check); :“(t : 1) * (Pl : check); :(Pl : pause);

14 >15 >$

bause,yleqFJ :(Pl : yleqF); :(Pl :pause);

15 >ll >$

{pause,checkj :(t : 1) * (Pl : check); zotherwise;

17

(pause,teq2) :(Pl : teq2); :(Pl : pause);

>18 >$ ACM Transactions

ALGORITHM

[lo : 0,ll: 1,12: 2,13 : 3,14 : 4,15 : 5,17 : 6,18: 71 [pause : 0,execute : l,yleqT : 2,check : 3,yleqF : 4,teq2 : 51

11 >12 =-$

13

OF DEKKER’S

/* The first process */

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines 18

l

329

bause,yleW :(Pl:yleqF); :(Pl:pause);

>lO >$ end process

P2

/* The second process */

import yl, t states 0..7 selections 0..5 init m0 trans m0 >ml >$ ml >m2 >$

valnm valnm

[mO: 0,ml: l,m2 : 2,m3 : 3,m4 : 4,m5 : 5,m7 : 6,m8: 71 [pause : 0,execute : l,y2eqT: 2,check: 3,y2eqF : 4,teql: 51

(pause,execute) :(P2 : execute); : (P2 : pause,execute); buw2eqTl :(P2:yBeqT); :(P2 : pause);

m2 >m7 >m3 =-$

(pause,check] :(yl:F) * (P2:check); ‘“(~1: F) * (P2 : check); I(P2 : pause);

m3 >m2 >m4 >$

(pause,check) :(t:2) * (P2:check); .“(t : 2) * (P2 : check); I(P2:pause);

m4 >m5 >$

bausw2eqFl :(P2 : y2eqF); : (P2 : pause);

m5 >ml >$

(pause,check) :(t : 2) * (P2 : check); :otherwise;

m7 >m8 >$

(pause,teql) :(P2; :teql) :(P2 : pause);

m8 >mO >$ end

bause,y24’1 : (P2 : y2eqF); :(P2:pause);

/* Private variable yl process yl import Pl valnm [F : 0,T : l] states O..l selections = states init F trans F >T:(Pl:yleqT); > F : otherwise;

*/

T >F:(Pl:yleqF); > T : otherwise; end ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

330

*

S. Aggarwal et al.

process y2 /* Private variable y2 */ import P2 states O..l valnm [F : 0,T : l] selections = states init F trans F >T : (P2 : y2eqT); > F : otherwise; T > F : (P2 : y2eqF); > T : otherwise; end /* The turn variable t */ process t import Pl, P2 states 1..2 selections = states init 1 trans >2: (Pl:teq2); >l:(P2:teql); > 1: otherwise; 2 > 1: (P2 : teql); > 2 : (Pl : teq2); > 2 : otherwise; end /* Liveness condition process LCl /* accepting set {l) */ import Pl states O..l selections = states init 0 trans 0 >O: (Pl:pause); > 1: otherwise;

for process one */

1 > 0 : (Pl : pause); >l : otherwise; end process LC2 /* Liveness condition /* accepting set (1) */ import P2 states O..l selections = states init 0 trans 0 > 0 : (P2 : pause); > 1: otherwise; ACM Transactions

on Programming

for process two */

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

l

331

1 >O : (P2 : pause); > 1: otherwise; end /* Task complement one */ process TCl /* accepting set (2) */ import Pl.$, P2.$ states L.2 selections = states init 1 trans 1 >2 :((P1.$:17) + (P1.$:18)) : otherwise; >l

* ((P2.$:m7)

+ (P2.$:m8));

2 >2

: true;

end process TC2 /* Task complement /* accepting set (1) */ import Pl.$ states 0..2 selections = states init 0 trans 0 : (Pl.$ : 11); >l :- (Pl.$: 11); P-0

two */

1 >2 >l

: (Pl.$ : 17); : -(Pl.$ : 17);

>2

: true;

2 end APPENDIX constants

8. FORMAL SPECIFICATION PROTOCOL

OF THE

ALTERNATING-BIT

n = 3

process S /* sender(l) */ /* generates messages to be sent to the receiver */ /* accepting set is (ONl) */ import SPtosender valm [OFF12 : O,ON12: l,ON2 : 2,OFF13 : 3,ON13 : 4,ON3 : states 0..7 5,OFFl: 6,ONl : 71 valm [idle : 0] selections O..n init OFF12 trans OFF12 (idle,l,2) >ON12 g;i’; : ; > ON2 : otherwise; =-$ ACM Transactions on Programming Languages and Systems, Vol. 12, No. 2, April 1990.

332

S. Aggatwal et al.

l

ON12 > OFF12 > ON12 ON2 > OFF13 > ON2

(idle) : (SP.tosender : done); : otherwise; ]idle] : (SP.tosender : done); : otherwise;

OFF13 >ON13 >ON3 =-$

(idle,l,3) ;;g:;;; : ; : otherwise;

ON13 > OFF13 >ON13

(idle) : (SP.tosender : done); : otherwise;

ON3 > OFF1 >ON3

(idle} : (SP.tosender : done); : otherwise;

OFF1 >ONl >$

(idle,11 :(S:l); : otherwise;

ON1 > OFF1 >ONl end cluster

mapping

/ * sending protocol cluster( 2) * /

SP

selections

{idle} : (SP.tosender : done); : otherwise;

tosender tochannel tosender tochannel

O..l O..l

valm valm

[done : 0, wait: l] [data: 1, nodata:O]

[done : (TR : ready); wait: otherwise;] [data: *(SB:empty) nodata: otherwise;]

* (TR:sent)

/* sending bufftr(2.1) */ prbcess SB /* buffers messages from sender until acknowledgment import S, TR valm [EMPTY : 0] states O..n valm [empty : 0] selections O..n init EMPTY trans EMPTY b-NY1 : (S : l..n); >s : (S : idle); >EMPTY -EMPTY > EMPTY >$ end

* (AA:nok);

received

*/

PI : (TR : ready); : otherwise;

/* transmitter(2.2) */ process TR /* controls the transmission and retransmission of the buffered message */ /* accepting set is {READY, WAITING] */ import AA, TR, S, TI valm [READY: 0,TRANS : l,WAITING : 21 states 0..2 valm [ready : 0,pause : 1,sent : 21 selections 0..2 init READY ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines trans READY >TRANS > READY TRANS > READY > WAITING >TRANS WAITING > READY >TRANS > WAITING end

l

333

beady1 : (S : l..n); : otherwise; (pause,sent] : (AA : ok); : (TR : sent) * “(AA : ok); : (TR : pause) * -(AA : ok); bus4 : (AA : ok); *-(AA:ok) * (TI:to); ;-(AA : ok) * “(TI : to);

/* timer(2.3) */ process TI /* indicates when retransmission should begin if no ack */ /* accepting set is (OFF, TO] */ import AA, TR valm [OFF : 0,ON : l,TO : 21 states 0..2 valm [off: 0,on : 1,to : 21 selections 0..2 init OFF trans OFF WI : (TR : sent); BON : otherwise; > OFF ON >OFF >TO >ON TO >OFF >ON >TO end

bOoI : (AA : ok); :(TI:to) * “(AA:ok); :(TI:on) * “(AA:ok); bol : (AA : ok); :*(AA:ok) * (TR:sent); :“(AA:ok) * “(TR: sent);

process SSN /* sending sequence number(2.4) */ /* this remembers the sequence number being sent */ import AA states O..l selections O..l init 0 trans $ ($1 : (AA : ok); >($+1)%2 : otherwise; >$ end process AA / * acknowledgment analyzer( 2.5) * / /* compares acknowledged sequence number with what was expected import CHI.tosp, CHI.RN, SSN valm [NOK:O,OK: l] states O..l selections O..l valm [nok : 0,ok : l] init NOK trans NOK bokJ : (SSN=CHI.RN) * (CHI.tosp : data); >OK > NOK : otherwise; ACM Transactions

on Programming

*/

Languages and Systems, Vol. 12, No. 2, April 1990.

334

’

S. Aggatwal et al.

OK >NOK end

bkl : (AA : ok);

endcluster cluster

/ * outgoing channel cluster( 3) * /

CHO

selections torp mapping torp

O..l valm [nodata : 0,data : l] [nodata: (M:pause,loss); data: (M: l..n);]

process M /* outgoing message type (3.1) */ /* holds message, then delivers or loses message */ import SP.tochannel, SP.SB valm [IDLE : 0] states O..n valm [pause : 0,loss : n+l] selections O..n+l init IDLE trans IDLE bus4 : (SP.tochannel : data); > SP.SB : (SP.tochannel : nodata); > IDLE {pause,loss,$) : (M : pause); :(M = $) + (M:loss);

-IDLE =-$ > IDLE end

/* outgoing channel sequence number(3.2) */ process SN /* keeps track of the outgoing message sequence number */ import SP.tochannel, SP.SSN, M valm [IDLE : 21 states 0..2 valm [pause : 21 selections 0..2 init IDLE trans IDLE bus4 : (SP.tochannel : data); > SP.SSN : (SP.tochannel : nodata); > IDLE “IDLE >$ > IDLE end

b§l : (M : pause); : otherwise;

process CHOLC /* monitor ensures CHO liveness condition(3.3) /* accepting set is (NORMAL, LOSTMOK) */ import SP.tochannel, M states 0..4 valm [NORMAL:O,GETM: l,LOSTMNOK: S,LOSTMOK:3,ERROR:4] selections O..O valm [pause : 0] init NORMAL trans NORMAL buf4 > GETM : (SP.tochannel: data); : otherwise; =+$ GETM > LOSTMNOK > LOSTMOK > NORMAL >$ ACM Transactions

k-4 : (M : loss); : (M : loss); : -(M : loss,pause); :(M:pause);

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

*/

Adding Liveness Properties to Coupled Finite-State Machines

bus4

LOSTMNOK > GETM >$

: (SP.tochannel : otherwise;

LOSTMOK >ERROR >$

bus4 : (SP.tochannel: : otherwise;

ERROR >ERROR end

.

335

: data);

data);

(pause1 : (CHOLC : pause);

endcluster cluster

CHI

selections tosp mapping tosp

/* incoming channel cluster(4)

*/

O..l valm [nodata : 0,data : l] [nodata : (ACK : pause,loss); data : (ACK : deliver);]

* mcoming acknowledgment message(4.1) process ACK import RP.tochar!rel states O..l valm [IDLE : 0,ACK : l] selections 0..2 valm [pause : 0,loss : 1,deliver : 21 init IDLE trans IDLE bus4 : (RP.tochannel: oldack,newack); >ACK : (RP.tochannel: nodata); > IDLE ACK >$ > IDLE end

(pause,loss,deliver) : (ACK : pause); : (ACK : deliver) + (ACK : loss);

/* incoming channel sequence number(4.2) process RN import RP.tochannel, RP.E, ACK valm [IDLE : 21 states 0..2 selections 0..3 valm [pause : 2,loss : 31 init IDLE trans IDLE (pause 1 : (RP.tochannel: nodata); > IDLE : (RP.tochannel : newack); > RP.E : (RP.tochannel: oldack); >(RP.E+l)%B “IDLE >$ > IDLE end

*/

*/

($1 : (ACK : pause); : otherwise;

/* monitor ensures CHI liveness condition(4.3) process CHILC /* accepting set is (NORMAL, LOSTMOK) */ import RP.tochannel, ACK valm [NORMAL:O,GETM: l,LOSTMNOK: states 0..4 2,LOSTMOK: 3,ERROR: 41 valm [pause : 0] selections O..O init NORMAL trans NORMAL Ipause1 : (RP.tochannel: oldack,newack); > GETM : otherwise; =-$ ACM Transactions

on Programming

*/

Languages and Systems, Vol. 12, No. 2, April 1990.

336

l

S. Aggarwal et al.

bus4

GETM > LOSTMNOK > LOSTMOK > NORMAL =-$

: (ACK : (ACK : -(ACK : (ACK

LOSTMNOK > GETM >$

bus4 : (RP.tochannel: : otherwise;

oldack,newack);

LOSTMOK > ERROR >$

bus4 : (RP.tochannel : otherwise;

: oldack,newack);

ERROR >ERROR end

: loss); : loss); : loss,pause); : pause);

b=-4 : (CHILC

: pause);

endcluster cluster

RP

/* receiving protocol cluster(5)

selections tochannel mapping tochannel

*/

0..2 valm [nodata : 0, newack : 1, oldack : 21 [nodata: (RB : empty); newack : “(RB : empty) * (MA : ok); oldack : -(RB : empty) * “(MA : ok);]

process RB /* receiving buffer(5.1) */ /* buffers the message received */ import CHO.torp, CH0.M valm [EMPTY : 0] states O..n selections O..n valm [empty : 0] init EMPTY trans EMPTY Iempty) >EMPTY : (CHO.torp: nodata); > CH0.M : (CHO.torp : data); -EMPTY > EMPTY end

($1 : (RB = $);

/* expected sequence number(5.2) */ process E / * remembers the receiver’s expected sequence number import MA, RB states O..l selections O..l init 0 trans $ ($1 : (MA : ok) * -(RB : empty); >($+1)%2 : otherwise; >$ end

*/

/* message analyzer(5.3) */ process MA /* analyzes the received message */ import CHO.torp, CHO.SN, E valm [NOK : 0,OK : l] states O..l selections O..l valm [nok : 0,ok : l] init NOK ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State lvlachines trans NOK >OK > NOK OK > NOK end

bkl

: (E=CHO.SN) : otherwise;

* (CHO.torp:

l

337

data);

bkl : (MA : ok);

endcluster /* receiver(g) */ process R /* represents the upper layer that actually gets the message */ import RP.MA, RP.RB states O..n valm [WAIT : 0] selections O..n valm [pause : 0] init WAIT trans WAIT bus4 : (RP.MA: ok) * (RP.RB != empty); > RP.RB > WAIT : otherwise; -WAIT > WAIT end

($1 : (R = $);

process TC /* complement of task to be proved(7) */ /* accepting set is (a,b,d,error) */ import R states 0..5 valm [a : 0,b : 1,c : 2,d : 3,dead : 4,error : 51 selections O..O valm [pause : 0] init a trans a bus4 >b : (R: 2); > error :(R:3); >a : otherwise; b >c > error >b

bus4 :(R:3); :(R:2); : otherwise;

> error >c >d

bausel : (R : 2,3); : (R: 1,pause); : (R : pause);

>d > dead

bu4 : (R : pause); : otherwise;

C

d

dead > dead

bus4 : (TC : pause);

error > error end

bus4 : (TC : pause); ACM Transactions

on Programming

Languages and Systems, Vol. 12, No. 2, April 1990.

338

l

S. Aggarwal et al.

REFERENCES 1. AGGARWAL, S., AND COURCOUBETIS, C. Distributed implementation of a model of communication and computation. In Proceedings of the 18th Hawaii Information Conference on System Sciences (Hawaii, Jan. 1985), pp. 206-218. 2. AGGARWAL, S., AND HAR’EL, Z. Simulation analysis of protocols in an integrated software environment. Comput. Networks ZSDN Syst. 163 (Jan. 1989), 197-215. 3. AGGARWAL, S., BARBARA, D., AND METH, K. Z. SPANNER-A tool for the specification, analysis, and evaluation of protocols. IEEE Trans. Softw. Eng. SE-13, 12 (Dec. 1987), 1218-1237. 4. AGGARWAL, S., BARBARA, D., AND METH, K. Z. A software environment for the specification and analysis of problems of coordination and concurrency. IEEE Trans. Softw. Eng. SE-14, 5 (Mar. 1988), 280-289. 5. AGGARWAL, S., KURSHAN, R. P., AND SABNANI, K. K. A calculus for protocol specification and validation. In Protocol Specification, Testing and Verification, ZZZ, H. Rudin, and C. H. West, Eds. North-Holland, Amsterdam, 1983, pp. 19-34. 6. AGGARWAL, S., KURSHAN, R. P., AND SHARMA, D. A language for the specification and analysis of protocols. In Protocol Specification, Testing and Verification, ZZZ, H. Rudin, and C. H. West, Eds. North-Holland, Amsterdam, 1983, pp. 35-50. 7. BARTLE~, K. A., SCANTLEBURY, R. A., AND WILKINSON, P. T. A note on reliable full-duplex transmission over half-duplex lines. Commun. ACM 12, 5 (May 1969), 260-261. 8. BUCHI, J. R. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Method and Philosophical Science 1960. Stanford University Press, Stanford, Calif., 1962, pp. l-12. 9. CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. Automatic vertification of finite-state concurrent systems using temporal logic specifications: A practical approach. In Proceedings of the 10th ACM Symposium on Principles of Programming Languages (Austin, Tex., Jan. 1984). ACM, New York, 1984, pp, 117-126. 10. CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. Automatic vertification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (1986), 244-263. 11. HAILPERN, B. T. Verifying concurrent processes using temporal logic. Ph.D. thesis, Stanford Univ., Stanford, Calif., 1980. 12. HAILPERN, B. T., AND OWICKI, S. S. Modular verification of computer communication protocols. IEEE Trans. Commun. COM-31,l (Jan. 1983). 13. KURSHAN, R. P. Modelling concurrent processes. In Proceedings of the American Mathematical Society Symposium on Applied Mathematics 31. American Mathematical Society, Providence, R.I., 1985. 14. KURSHAN, R. P., AND GOPINATH, B. The selection/resolution model for concurrent processes. Unpublished. 15. LICHTENSTEIN, O., AND PNUELI, A. Checking that finite state concurrent programs satisfy their linear specifications. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan. 1985). ACM, New York, 1985, pp. 97-107. 16. MANNA, Z., AND PNUELI, A. Verification of concurrent programs: The temporal framework. In The Correctness Problem in Computer Science, Boyer and Moore, Eds. Academic Press, New York, 1981. 17. MANNA, Z., AND PNUELI, A. Verification of concurrent programs: Temporal proof principals. In Logics of Programs Proceedings. Lecture Notes in Computer Science, vol. 131. Springer-Verlag, New York, 1982, pp. 200-252. 18. MANNA, Z., AND WOLPER, P. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6 (1984). 19. MCNAUGHTON, R. Testing and generating infinite sequences by a finite automata. Znf. Control 9 (1966), 521-530. 20. PNUELI, A. The temporal logic of programs. In Proceedings of the 18th Symposium on Foundations of Computer Science (Providence, RI., Nov. 1977). 1977, pp. 46-57. 21. SABNANI, K. An algorithmic technique for protocol verification. ZEEE Trans. Commun. To be published. ACM Transactions on Programming Languages and Systems, Vol. 12, No. 2, April 1990.

Adding Liveness Properties to Coupled Finite-State Machines

l

339

22. SABNANI, K., WOLPER, P., AND LAPONE, A. An algorithmic technique for protocol verification. In Proceedings of the IEEE Globecom (New Orleans, La., Dec. 1985). IEEE, New York, 1985. 23. SUNSHINE, C. A., ED. Communication Protocol Modeling. Artech House, Dedham, Mass., 1981. 24. VARDI, M. Y., AND WOLPER, P. An automata-theoretic approach to automatic program verification. In Proceedings of the Symposium on Logic in Computer Science (Cambridge, Mass., June 1986). pp. 322-331. 25. WOLPER, P. Synthesis of communicating processes from temporal logic specifications. Ph.D. thesis, Stanford Univ., Stanford, Calif., 1982. 26. WOLPER, P. Temporal logic can be more expressive. Znf. Control 56, 1-2 (Jan. 1983), 72-99. 27. WOLPER, P. Specifying interesting properties of programs in propositional temporal logic. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages (St. Petersburg Beach, Fla., Jan. 1986). ACM, New York, 1986, pp. 184-193. 28. WOLPER, P., VARDI, M. Y., AND SISTLA, A. P. Reasoning about infinite computation paths. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science (Tucson, Ariz.). IEEE, New York, 1983, pp. 185-194.

Received October 1986; revised January

1989 and July 1989; accepted August 1989

ACM Transactions on Programming Languages and Systems, Vol. 12, No. 2, April 1990.