APPLICATIONS 93

4.2.1 Analysis Complexity

If the states in the CTL structure are correctly labeled with arg1 and arg2 of f , function auf requires time O(number of states in CTL structure+number of transitions). Since each pass through the main loop takes time O(number of states in CTL structure + number of transitions), the entire model checker requires O(length( f ) , (number of states in CTL structure + number of transitions)).

4.3 EXTENSIONS TO CTL

Extensions to CTL are needed to handle the verification of correctness along fair execution sequences and to specify absolute time instead of relative ordering of events. Here, we discuss how to extend CTL to handle fairness properties. For example, with a real-time rule-based program, we would like to consider the execution paths (sequences of rule firings) in which enabled rules are equally likely to be selected for execution, that is, a fair scheduler is assumed. Similarly, with a collection of concurrent processes, we would like to consider only the computation paths in which each process is executed infinitely often. In general, a fairness condition asserts that requests for service are granted sufficiently often [Garbay et al., 1980]. Many definitions exist of “requests” and “sufficiently often.” Here, we say a path is fair if enabled events in each state along the path are equally likely to happen.

CTL cannot express the correctness of fair executions. More precisely, the property that some proposition P should eventually hold on all fair executions cannot be specified in CTL. To handle fairness while maintaining an efficient model checking algorithm, we modify the semantics of CTL [Clarke, Emerson, and Sistla, 1986] to yield a new logic called CTL-F. It has the same syntax but a structure is now a 4-tuple (S, R, P, F), where S, R, P have the same meaning as described earlier and F is a collection of predicates on S. A path is F-fair iff for each g F, infinitely many states on the path satisfy predicate g. In CTL-F, all path quantifiers range over fair paths but the semantics remain the same as in CTL. For any given finite structure M = (S, R, P), collection F = G1, . . . , Gn of subsets of S, and state s0 S, there exists an F-fair path in M starting at s0 iff there exists a strongly connected component C of the graph of M such that (1) a finite path exists from s0 to a state t C and (2) for each Gi a state ti C ∩ Gi exists.

4.4 APPLICATIONS

One application of a model checker is to determine whether a program will terminate, that is, reach a fixed point, under all conditions. For instance, the module mcf in [Browne, Cheng, and Mok, 1988] (described in chapter 10) is a temporal logic model checker based on the Clarke–Emerson–Sistla algorithm for checking the satisfiability of temporal logic formulas written in CTL. Our model checker assumes that strong fairness is observed by the scheduler, that is, rules that are enabled infinitely often will eventually fire. Under this assumption, a cycle in the state space

94 MODEL CHECKING OF FINITE-STATE SYSTEMS

graph that has at least one edge exiting from it is sufficient to allow the program to reach a fixed point in a finite number of iterations. (The program will leave the states in the cycle because the rule associated with the exit edge must eventually fire.) However, the model checker will warn the designer that the program may require a finite but unbounded number of iterations to reach a fixed point.

4.4.1 Analysis Example

We now describe how a model checker can be applied to determine whether a rulebased program written in the EQL (equational logic) language (described in chapter 10) will always terminate. The purpose of the following program is to determine whether an object is detected at each monitor-decide cycle. The system consists of two processes and an external alarm clock which invokes the program by periodically setting the variable wakeup to true.

(* Example EQL Program *) PROGRAM distributed; CONST

false = 0; true = 1; a = 0;

b = 1; VAR synca, syncb, wakeup,

objectdetected : BOOLEAN; arbiter : INTEGER; INPUTVAR

sensora,

sensorb : INTEGER; INIT

synca := true, syncb := true, wakeup := true,

objectdetected := false, arbiter := a

RULES

(* process A *)

objectdetected := true ! synca := false

IF (sensora = 1) AND (arbiter = a) AND (synca = true) [] objectdetected := false ! synca := false

IF (sensora = 0) AND (arbiter = a) AND (synca = true) [] arbiter := b ! synca := true ! wakeup := false

IF (arbiter = a) AND (synca = false) AND (wakeup = true)

(* process B *)

[] objectdetected := true ! syncb := false

IF (sensorb = 1) AND (arbiter = b) AND (syncb = true)

96 MODEL CHECKING OF FINITE-STATE SYSTEMS

input and program variable values. This formula, together with the representation of the labeled state–space graph, is the input to the model checker and the timing analyzer.

The temporal logic model checker can now be used to determine whether a fixed point is always reachable in a finite number of iterations by analyzing this finite state–space graph with the given initial state. To verify that the program will reach a fixed point from any initial state, the reachability graph of every initial state must be analyzed by the model checker. The complete state–space graph of the example EQL program, which consists of eight separate finite reachability graphs, one for each distinct initial state, is shown in Figure 10.5 in Chapter 10. For example, the graph with initial state (t, t, t, −, a, 0, 1), corresponding to the combination of input values and initial program values, is one of 23 = 8 possible graphs that must be checked by the model checker.

In general, for a finite-domain EQL program with n input variables and m program variables, the total number of reachability graphs that have to be checked in the worst case (i.e., all combinations of the values of the input and program vari-

be checked is substantially less because many combinations of input and program variable values do not constitute initial states.

4.5 COMPLETE CTL MODEL CHECKER IN C

/*===========================================================================*/

98 MODEL CHECKING OF FINITE-STATE SYSTEMS

#define atomic 0 #define nt 1 #define ad 2 #define ax 3 #define ex 4 #define au 5 #define eu 6

typedef byte operatortype; typedef struct item *itemptr; struct item

{

short ip; itemptr next;

};

typedef char codetype[2]; struct optype

{

short p; operatortype opcode; codetype op;

};

typedef byte graphtype[maxstates+1][maxstates+1]; typedef struct optype ftype[maxflength];

typedef codetype fcode[maxflength+1]; typedef fcode flabeltype[maxstates+1];

typedef Boolean labeltype[maxflength][maxstates+1]; struct flist

{

short arg1, arg2;

};

typedef ftype nftype[maxflength]; typedef struct flist sftype[maxflength]; typedef Boolean marktype[maxstates+1];

/*---------------------------------------------------------------------------*/

graphtype e; /* global state transition graph */ labeltype labeled; /* indicates which formulas are */ /* labeled in each state */

nftype nf; /* array of subformulas numbered */

/* in the order they appear in */

/* the original formula */

sftype sf; /* gives the list of arguments, if */ /* any, of each subformula operator*/

ftype formula; /* input formula to be proved */ marktype marked; /* indicates which states in the */ /* state transition graph have been */

/* visited in procedure labelgraph */

/*===========================================================================*/

/*===========================================================================*/

/* function typeoperator (op) */ operatortype typeoperator (_op) codetype _op;

{

codetype op;

operatortype _typeoperator; ARRAYcopy(_op,op,sizeof(op));

if ((op[0] != ’a’) && (op[0] != ’e’) && (op[0] != ’n’)) _typeoperator = atomic;

else {

switch(op[0])

{

case ’a’:

if ((op[1] != ’d’) && (op[1] != ’u’) && (op[1] != ’x’)) _typeoperator = atomic;

else {

switch(op[1])

{

case ’d’:

_typeoperator = ad; break;

case ’u’:

_typeoperator = au; break;

case ’x’:

_typeoperator = ax; break;

}

}

break;

/*

#---------------------------------------------------------

*/ case ’e’:

if (op[1] == ’u’) _typeoperator = eu;

else if (op[1] == ’x’) _typeoperator = ex;

else _typeoperator = atomic; break;

/*

#---------------------------------------------------------

100 MODEL CHECKING OF FINITE-STATE SYSTEMS

*/ case ’n’:

if (op[1] == ’t’)

_typeoperator = nt;

else _typeoperator = atomic;

break;

}

}

return(_typeoperator);

}

/*typeoperator*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure readgraph (e,numstates) */ readgraph (e,numstates)

graphtype e; short *numstates;

{

short i, j;

fprintf(stdout," Please enter the number of states in the graph:"); writeln(stdout);

writeln(stdout);

fscanf(stdin,"%d",numstates);

readln(stdin);

*numstates = *numstates - 1;

fprintf(stdout," Please enter graph in adjacency matrix form:"); writeln(stdout);

writeln(stdout);

for (i=0; i <= maxstates; i++) for (j=0; j <= maxstates; j++)

e[i][j] = 0;

for (i=0; i <= *numstates; i++)

{

for (j=0; j <= *numstates; j++) fscanf(stdin,"%d",&e[i][j]);

readln(stdin);

}

fprintf(stdout," ");

for (i=0; i <= *numstates; i++) fprintf(stdout,"%3d",i);

writeln(stdout);

for (i=0; i <= *numstates; i++)

{

fprintf(stdout,"%3d",i);

for (j=0; j <= *numstates; j++) fprintf(stdout,"%3d",e[i][j]);

writeln(stdout);

}

writeln(stdout);

}

/*readgraph*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure readlabel (flabel) */ readlabel (flabel)

flabeltype flabel;

{

char symbol; short i, j, s;

fprintf(stdout," Please enter the initial labels in the following form: "); writeln(stdout);

# Read in the initial labels for each state.

#------------------------------------------------------------------------

*/

for (s=0; s <= numstates; s++)

{

fscanf(stdin,"%d",&i); symbol = getc(stdin); j = 1;

while (symbol != ’;’)

{

if (symbol != ’ ’)

{

flabel[s][j][0] = symbol; flabel[s][j][1] = getc(stdin); j = j + 1;

}

symbol = getc(stdin);

}

readln(stdin);

writeln(stdout); fprintf(stdout,"%3d ",s); j = 1;

while (flabel[s][j][0] != ’ ’)

{

putc(flabel[s][j][0],stdout); fprintf(stdout,"%c ",flabel[s][j][1]); j = j + 1;

}

102 MODEL CHECKING OF FINITE-STATE SYSTEMS

}

writeln(stdout);

writeln(stdout);

}

/*readlabel*/

/*===========================================================================*/

/* procedure printheading */

/*===========================================================================*/

}

/*printheading*/

/*===========================================================================*/

/* procedure printoutput */

/*===========================================================================*/

/* procedure printoutput */ printoutput ()

{

short i, j; /*

#-------------------------------------------------------------------------

# First, print out the numbered input formula.

fprintf(stdout,"%3d",i);

writeln(stdout); putc(’ ’,stdout);

for (i=1; i <= flength; i++)

fprintf(stdout," The formula is proved to be true. "); writeln(stdout);

}

else {

fprintf(stdout," The formula is proved to be false. "); writeln(stdout);

}

}

/*printoutput*/

/*===========================================================================*/

/*===========================================================================*/

104 MODEL CHECKING OF FINITE-STATE SYSTEMS

/* procedure push (p,top) */ push (p,top)

short p; itemptr *top;

{

itemptr node;

node = (itemptr)malloc(sizeof(struct item)); node->ip = p;

node->next = *top; *top = node;

}

/*push*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure pop (p,top) */ pop (p,top)

short *p; itemptr *top;

{

itemptr temp;

*p = (*top)->ip; temp = *top;

*top = (*top)->next; free(temp);

}

/*pop*/

/*===========================================================================*/

/*===========================================================================*/

/* function empty (top) */ Boolean empty (top) itemptr top;

{

Boolean _empty;

if (top == (itemptr)(NULL)) _empty = true;

else _empty = false;

return(_empty);

}

/*empty*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure readf (f,flength,s) */ readf (f,flength,s)

ftype f;

short *flength, *s;

{

itemptr ptop; /* top of the stack of numbers corresponding */ /* to parentheses found in the input formula */

short i, j, ip, lp; /* number of left parentheses read */ char lastsymbol, symbol; /* the input character */

fprintf(stdout," Please enter the formula to be in proved in prefix form:"); writeln(stdout);

writeln(stdout);

ptop = (itemptr)(NULL);

for (i=1; i <= maxflength; i++)

{

f[i-1].p = 0; f[i-1].opcode = atomic; for (j=1; j <= 2; j++)

f[i-1].op[j-1] = ’ ’;

}

i = 1;

symbol = getc(stdin); /*

#-------------------------------------------------------------------------

#If the formula is not atomic, then the following code insures that

#all subformulas will be read properly.

#-------------------------------------------------------------------------

*/

if (symbol == ’(’)

{

lp = 1;

f[i-1].p = lp;

push(lp,&ptop);

while (!empty(ptop))

{

if (symbol != ’ ’) lastsymbol = symbol;

symbol = getc(stdin); if (symbol == ’(’)

{

lp = lp + 1; f[i-1].p = lp;

106 MODEL CHECKING OF FINITE-STATE SYSTEMS

push(lp,&ptop);

}

else if (symbol == ’)’)

{

if (lastsymbol != ’)’) i = i - 1;

pop(&ip,&ptop); f[i-1].p = ip;

}

else if (symbol != ’ ’)

{

f[i-1].op[0] = symbol; symbol = getc(stdin);

if (((symbol >= ’a’)&&(symbol <= ’z’))||((symbol >= ’0’)&&(symbol <= ’9’)))

f[i-1].op[1] = symbol;

f[i-1].opcode = typeoperator(f[i-1].op); i = i + 1;

}

}

*flength = i;

}

else

/*

#------------------------------------------------------------------

# If the formula is atomic, indicate that its length is one.

#------------------------------------------------------------------

*/ {

f[i-1].op[0] = symbol; symbol = getc(stdin);

if (((symbol >= ’a’) && (symbol <= ’z’)) || ((symbol >= ’0’) && (symbol <= ’9’)))

f[i-1].op[1] = symbol; *flength = 1;

}

readln(stdin);

fprintf(stdout," Please enter the state at which the formula is to be proved:");

writeln(stdout);

writeln(stdout);

fscanf(stdin,"%d",s);

readln(stdin);

for (i=1; i <= *flength; i++)

{

putc(f[i-1].op[0],stdout); fprintf(stdout,"%c ",f[i-1].op[1]);

}

writeln(stdout); fprintf(stdout,"state = %d",*s); writeln(stdout); writeln(stdout);

}

/*readf*/

108 MODEL CHECKING OF FINITE-STATE SYSTEMS

*/

if (f[fi-1].opcode != atomic)

{

do {

j = j + 1; i = i + 1;

nf[fi-1][j-1].op[0] = f[i-1].op[0]; nf[fi-1][j-1].op[1] = f[i-1].op[1]; nf[fi-1][j-1].opcode = f[i-1].opcode; nf[fi-1][j-1].p = f[i-1].p;

} while (!(f[i-1].p <= lp));

/*

#---------------------------------------------------------------

#Now compute the values of array sf - the number(s)

#corresponding to the argument(s) of operator f[fi].opcode. If

#the opcode is unary -- nt, ax, and ex, then only one argument

#number is determined.

#---------------------------------------------------------------

*/

i = fi + 1; sf[fi-1].arg1 = i;

if ((f[fi-1].opcode != nt) && (f[fi-1].opcode != ax) && (f[fi-1].opcode != ex))

{

if (f[i-1].opcode == atomic) sf[fi-1].arg2 = i + 1;

else {

lp = f[i-1].p; do {

i = i + 1;

} while (!(f[i-1].p <= lp)); sf[fi-1].arg2 = i + 1;

}

}

}

}

/*do*/

writeln(stdout); fprintf(stdout," Array sf:"); writeln(stdout);

for (i=1; i <= fl; i++)

{

fprintf(stdout,"%3d %4d %4d",i,sf[i-1].arg1,sf[i-1].arg2); writeln(stdout);

}

writeln(stdout);

}

/*buildnfsf*/

/*===========================================================================*/

/*===========================================================================*/

/* function initlabeled (s,f) */ Boolean initlabeled (s,_f) short s;

ftype _f;

{

ftype f;

Boolean _initlabeled; short i;

Boolean b;

ARRAYcopy(_f,f,sizeof(f));

/*

#---------------------------------------------------------------------------

#If the opcode is atomic, meaning that it is a single atomic

#proposition, then we only need to find it in state s by looking

#at the flabel (array of initial labels in character form).

#If found, b is set to true, else false.

#---------------------------------------------------------------------------

*/

if (f[0].opcode == atomic)

{

b = false; i = 0;

while ((!b) && (flabel[s][i][0] != ’ ’))

{

if ((flabel[s][i][0] == f[0].op[0]) && (flabel[s][i][1] == f[0].op[1]))

b = true; i = i + 1;

}

}

/*

#------------------------------------------------------------------------

#If the opcode is nt (not), then we have to search the whole array

#flabel to see if the input label is there. If it is found, then

#b is set to false, else true.

#------------------------------------------------------------------------

*/ else if (f[0].opcode == nt)

{

b = true;

i = 0;

while (b && (flabel[s][i][0] != ’ ’))

110 MODEL CHECKING OF FINITE-STATE SYSTEMS

{

if ((flabel[s][i][0] == f[0].op[0]) && (flabel[s][i][1] ==

f[0].op[1]))

b = false;

i = i + 1;

}

}

else b = false; return(b);

}

/*initlabeled*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure addlabel (s,fi,labeled) */ addlabel (s,fi,labeled)

short s, fi; labeltype labeled;

{

labeled[s][fi-1] = true;

}

/*===========================================================================*/

/*===========================================================================*/

/* procedure initsystem */ initsystem ()

{

short i, s;

for (s=0; s <= maxstates; s++)

{

/*

#---------------------------------------------------------------------

# Assign label t (true) to every state since t is true everywhere.

#---------------------------------------------------------------------

*/

flabel[s][0][0] = ’t’; flabel[s][0][1] = ’ ’;

for (i=1; i <= maxflength; i++)

{

labeled[s][i-1] = false; flabel[s][i][0] = ’ ’; flabel[s][i][1] = ’ ’;

}

}

}

/*initsystem*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure atf (fi,s,b) */ atf (fi,s,b)

short fi, s; Boolean *b;

{

short s1;

for (s1=0; s1 <= numstates; s1++)

if (labeled[s1][fi-1] || initlabeled(s1,nf[fi-1])) if (!labeled[s1][fi-1])

addlabel(s1,fi,labeled); if (labeled[s][fi-1])

*b = true; else *b = false;

}

/*atf*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure ntf (fi,s,b) */ ntf (fi,s,b)

short fi, s; Boolean *b;

112 MODEL CHECKING OF FINITE-STATE SYSTEMS

{

short s1, a1;

a1 = sf[fi-1].arg1;

for (s1=0; s1 <= numstates; s1++)

if (!(labeled[s1][a1-1]) || initlabeled(s1,nf[a1-1])) addlabel(s1,fi,labeled);

if (labeled[s][fi-1]) *b = true;

else *b = false;

}

/*ntf*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure adf (fi,s,b) */ adf (fi,s,b)

short fi, s; Boolean *b;

{

short s1, a1, a2; a1 = sf[fi-1].arg1; a2 = sf[fi-1].arg2;

for (s1=0; s1 <= numstates; s1++)

if (labeled[s1][a1-1] || initlabeled(s1,nf[a1-1]))

if (labeled[s1][a2-1] || initlabeled(s1,nf[a2-1]))

addlabel(s1,fi,labeled);

if (labeled[s][fi-1])

*b = true;

else *b = false;

}

/*adf*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure axf (fi,s,b) */ axf (fi,s,b)

short fi, s; Boolean *b;

{

Boolean b1; short s1, s2, a1;

a1 = sf[fi-1].arg1;

for (s1=0; s1 <= numstates; s1++)

{

b1 = true;

s2 = 0;

while (b1 && (s2 <= numstates))

{

if ((s1 != s2) && (e[s1][s2] == 1))

if (!(labeled[s2][a1-1] || initlabeled(s2,nf[a1-1]))) *b = false;

s2 = s2 + 1;

}

if (b1) addlabel(s1,fi,labeled);

}

if (labeled[s][fi-1]) *b = true;

else *b = false;

}

/*axf*/

/*===========================================================================*/

/* arg1, then label state s with (ex arg1) and return true, else false. */ /*===========================================================================*/

/* procedure exf (fi,s,b) */ exf (fi,s,b)

short fi, s; Boolean *b;

{

Boolean b1; short s1, s2, a1;

a1 = sf[fi-1].arg1;

for (s1=0; s1 <= numstates; s1++)

{

b1 = false;

s2 = 0;

while ((!b1) && (s2 <= numstates))

114 MODEL CHECKING OF FINITE-STATE SYSTEMS

{

if ((s1 != s2) && (e[s1][s2] == 1))

if (labeled[s][a1-1] || initlabeled(s,nf[a1-1]))

{

b1 = true; addlabel(s2,fi,labeled);

}

s2 = s2 + 1;

}

}

if (labeled[s][fi-1]) *b = true;

else *b = false;

}

/*exf*/

/* procedure dfs (s2,f1) */ dfs (s2,f1)

short s2, f1;

{

short s1; addlabel(s2,fi,labeled);

for (s1=0; s1 <= numstates; s1++)

if ((s1 != s2) && (e[s1][s2] == 1))

if (labeled[s1][a1-1] || initlabeled(s1,nf[a1-1]))

if (!labeled[s1][fi-1])

dfs(s1);

}

/*dfs*/

/*===========================================================================*/

/*===========================================================================*/

/* procedure euf (fi,s,b) */ euf (fi,s,b)

short fi, s; Boolean *b;

{

short s2, a1, a2; /*

#-------------------------------------------------------------------------

#For all states which are labeled with arg2, perform a depth first

#search to label all states in paths which have prefix arg1 and end

#state labeled with arg2. If state s is labeled with (eu arg1 arg2),

#then return b = true, else false.

#-------------------------------------------------------------------------

*/

a1 = sf[fi-1].arg1;

a2 = sf[fi-1].arg2;

for (s2=0; s2 <= numstates; s2++)

if (labeled[s2][a2-1] || initlabeled(s2,nf[a2-1])) dfs(s2,fi);

if (labeled[s][fi-1]) *b = true;

else *b = false;

}

/*euf*/

/*===========================================================================*/

/* procedure auf - shown above */

/*===========================================================================*/

/*===========================================================================*/

/* procedure labelgraph - shown above */

/*===========================================================================*/

/*===========================================================================*/

/*===========================================================================*/

main(argc, argv) int argc;

char **argv;

{

printheading();

initsystem();