Improving the precision of INCA by preventing spurious cycles.
The Inequality Necessary Condition Analyzer (INCA) is a finite-state  verification tool that has been able to check properties of some  very large concurrent systems. INCA checks a property of a  concurrent system by generating a system of inequalities that must  have integer solutions if the property can be violated. There may,  however, be integer solutions to the inequalities that do not  correspond to an execution violating the property. INCA thus accepts  the possibility of an inconclusive result in exchange for greater  tractability. We describe here a method for eliminating one of the two main sources of these inconclusive results.
INTRODUCTION
Finite-state verication tools deduce properties of nite-
state models of computer systems. They can be used to
check such properties as freedom from deadlock, mutually
exclusive use of a resource, and eventual response to a re-
quest. If the model represents all the executions of a system
(perhaps by making use of some abstraction), a nite-state
verication tool can take into account all the executions of
Research partially supported by the National Science Foundation
under grant CCR-9708184. The views, ndings, and
conclusions presented here are those of the authors and
should not be interpreted as necessarily representing the ocial
policies or endorsements, either expressed or implied, of
the National Science Foundation, or the U.S. Government.
the system. Moreover, nite-state verication tools can be
applied at any stage of system development at which an appropriate
model can be constructed. Such tools thus represent
an important complement to testing, especially for concurrent
systems where nondeterministic behavior can lead to
very dierent executions arising from the same input data.
The main obstacle to nite-state verication of concurrent
systems is the state explosion problem: the number of states
a concurrent system can reach is, in general, exponential
in the number of concurrent processes in the system. This
problem confronts the analyst immediately|even for small
systems, the number of reachable states can be large enough
so that a straightforward approach that examines each state
is completely infeasible|and complexity results tell us that
there is no way to avoid it completely. Every method for
nite-state verication of concurrent systems must pay some
price, in accuracy or range of application, for practicality.
The Inequality Necessary Conditions Analyser (INCA) is
a nite-state verication tool that has been used to check
properties of some systems with very large state spaces. The
INCA approach is to formulate a set of necessary conditions
for the existence of an execution of the program that violates
the property. If the conditions are inconsistent, no
execution can violate the property. If the conditions are
consistent, the analysis is inconclusive; since the conditions
are necessary but not su-cient, it may still be the case that
no execution of the program can violate the property. INCA
thus accepts the possibility of an inconclusive result in exchange
for greater tractability. There are two main sources
of inconclusive results. In this paper, we show how one of
these, caused by cycles in nite state automata representing
the components of the concurrent system, can be eliminated
at what seems to be only moderate cost.
In the next section, we describe the INCA approach. Section
3 explains our technique for improving INCA's preci-
sion, and the fourth section presents some preliminary data
on its application. The nal section summarizes the paper
and discusses other issues related to the precision of INCA.
2. INCA
A complete discussion of the INCA approach, along with a
careful analysis of its expressive power, is contained in [8]. In
this paper, we will use a small (and quite contrived) example
to sketch the basic INCA approach and show how certain
cycles in the automata corresponding to the components of
a concurrent system can lead to imprecision in the INCA
analysis. We refer readers who want more detail to [8].
2.1 Basic Approach
The basic INCA approach is to regard a concurrent system
as a collection of communicating nite state automata
Transitions between states in these FSAs correspond
to events in an execution of the system. INCA treats
each FSA as a network with
ow, and regards each occurrence
of a transition from state s to state t, corresponding
to an event e, as a unit of
ow from node s to node t. The
sequence of transitions in a particular FSA corresponding
to events in a segment of an execution of the system thus
represents a
ow from one state of the FSA to another.
To check a property of a concurrent system using INCA, an
analyst species the ways that an execution might violate
the property in terms of a sequence of segments of an exe-
cution. Suppose that an analyst wants to show that event
b can never be preceded by event a in any execution of the
system. A violation of this property is an execution in which
a occurs and then b occurs. In INCA this could be specied
as a single segment running from the start of the execution
until the occurrence of a b, with the requirement that an a
occur somewhere in the segment. (It could also be specied
as a sequence of two segments, the rst running from the
start of the execution until an occurrence of an a, and the
second starting immediately after the rst and ending with
a b. The former specication is generally more e-cient, but
the latter may provide additional precision in some cases.
See Section 2.2.) INCA provides a query language allowing
the analyst to specify various aspects of the segments (called
\intervals" in the INCA query language) of execution.
By generating the equations describing
ow within each FSA
(requiring that the
ow into a node equal the
ow out) according
to the specied sequence of segments of a system
execution, and adding equations and inequalities relating
certain transitions in dierent FSAs according to the semantics
of communication in the system, INCA produces a
system of equations and inequalities. Any execution that
satises the analyst's specication (and therefore violates
the property being checked) corresponds to an integer solution
of this system of equations and inequalities. INCA then
uses standard integer linear programming (ILP) methods to
determine whether there is an integer solution. If no integer
solution exists, no execution can violate the property, and
the property holds for all executions of the concurrent sys-
tem. If there is an integer solution, however, we do not know
that the property can be violated. The system of equations
and inequalities represents only necessary conditions for the
existence of an execution violating the property, and it is
possible for a solution to exist that does not correspond to
a real execution.
To see more concretely how this works, consider the Ada
program shown in Figure 1. This program describes three
concurrent processes (tasks). Task t1 begins by rendezvous-
ing with task t2 at the entry c. It then enters a loop. At
the select statement, t1 nondeterministically chooses to rendezvous
with t2 at entry a or with t3 at entry b, if both are
ready to communicate at the appropriate entries. If t1 ac-
package simple is
task t1 is task t2 is
entry a; end t2;
entry b;
entry c; task t3 is
package body simple is
task body t1 is task body t2 is
begin begin
accept c; t1.c;
loop loop
select t1.a;
accept a; end loop;
loop end t2;
select
accept a;
or
accept c;
exit; task body t3 is
or end t3;
accept b;
loop
accept a;

Figure

1: A small example
cepts a communication from t2 at entry a, it then enters a
loop in which it accepts rendezvous at entry a until it accepts
one at entry c. If t1 instead accepts a communication from
t3 at entry b, it then tries forever to repeatedly rendezvous
with t2 at entry a.

Figure

2 shows the FSAs constructed by INCA for this pro-
gram. The states and transitions are numbered for reference.
Each transition in this example represents the occurrence of
a rendezvous between two tasks; in the gure, each transition
is labeled with the entry at which the corresponding
rendezvous takes place.
Suppose that we wish to check that an occurrence of a rendezvous
at entry b cannot be preceded by a rendezvous at
entry a. As described earlier, we may specify the violation as
a segment of an execution running from the start of execution
until the occurrence of a rendezvous at b and containing
a rendezvous at a. The
ow equations for each task will then
describe the possible
ows from the initial state of the task
to one of the states in which that task could be at the end
of the segment.
Since the segment ends with a rendezvous at the entry b,
represented by the transition numbered 2 in the FSA corresponding
to task t1 and the transition numbered 9 in the
FSA corresponding to task t3, we know that the FSA t1
must be in state 3 and the FSA t3 must be in state 8 at
the end of the segment. Our
ow equations for t1 therefore
describe
ow starting in state 1 and ending in state 3, while
the
ow equations for t3 describe
ow starting in state 7
and ending in state 8. For t2, the fact that a rendezvous at
a occurs in the segment implies that that FSA must be in
state 6 at the end of the segment, so the
ow equations for
t2 describe
ow from state 5 to state 6.
To produce these
ow equations, let x i be a variable measur-
a
c
a
a
a

Figure

2: FSAs for example
ing the
ow along the transition numbered i. At each state,
we generate an equation setting the
ow in equal to the
ow
out. We must, however, take into account the implicit
ow
of 1 into the initial state of each FSA and the implicit
ow
of 1 out of the end state of the
ow. Thus, for example, the
equation for state 1 is
since the
ow in is 1 because state 1 is the initial state and
the only
ow out is on transition 1. Similarly, the equation
for state 8 is
since the only
ow in is on transition 9 and there is implicit
ow out of 1 since the
ow in this FSA ends in state 8.
To complete the system of equations and inequalities, we
must add equations to re
ect the fact that the two tasks
participating in a rendezvous must agree on the number of
times it occurs. For instance, we need the equation
saying that the number of occurrences of the rendezvous at
entry a in the FSA for t1 is the same as in the FSA for t2.
We also need an inequality to express the requirement that
there is at least one occurrence of a rendezvous at a. We use
to state this. The full system of equations and inequalities
used to check the property that a rendezvous at entry b
cannot be preceded by a rendezvous at entry a is shown in

Figure

3. (The description here is actually somewhat over-
simplied; INCA performs several optimizations to reduce
the size of the system of inequalities and the real system of
inequalities produced by INCA would be smaller. For ex-
ample, INCA would observe that there cannot be
ow along
transition 3 in a violating execution (because the segment
of execution must end with transition 2), and would eliminate
the variable x3 from the system. It would also do a
form of constant propagation to eliminate other variables
and equations.)
Essentially all research on nite-state verication tools can
Flow Equations:
State Equation
Communication Equations:
Entry Equation
a x3
Requirement Inequality:
a occurs x8  1

Figure

3: System of equations and inequalities for
example
be viewed as aimed at ameliorating the state explosion problem
for some interesting systems and properties. The approach
taken by INCA avoids enumerating the reachable
states of the system and is inherently compositional, in the
sense that that the equations and inequalities are generated
from the automata corresponding to the individual
processes, rather than from a single automaton representing
the full concurrent system. The size of the system of
equations and inequalities is essentially linear in the number
of processes in the system (assuming the size of each
process is bounded). Furthermore, the use of properly chosen
cost functions in solving the problems can guide the
search for a solution. ILP is itself an NP-hard problem in
general, and the standard techniques for solving ILP problems
(branch-and-bound methods) are potentially exponen-
tial. In practice, however, the ILP problems generated from
concurrent systems have large totally unimodular subproblems
and seem particularly easy to solve. Experience suggests
that the time to solve these problems grows approximately
quadratically with the size of the system of inequalities
(and thus with the number of processes in the system).
Comparisons of this approach with other nite-state verica-
tion methods [2, 3, 4, 5] show that the performance of each
method varies considerably with the system and property
being veried, but that INCA frequently performs as well
as, or better than, such tools as SPIN and SMV. The INCA
approach has also been extended to check timing properties
of real-time systems [1, 6] and to prove trace equivalence of
certain classes of systems [7].
2.2 Sources of Imprecision
The systems of equations and inequalities generated by INCA
represent necessary conditions for there to be a violation of
the property being veried. As noted earlier, however, they
only represent necessary, not su-cient, conditions. A solution
of the system of equations and inequalities may not
correspond to an actual execution.
There are two main reasons for this. The rst has to do with
the order in which events occur. Strictly speaking, the equations
and inequalities generated by INCA refer only to the
total number of occurrences of the various events in each
segment of the execution, and do not directly impose restrictions
on the order in which those events occur within
the segment. In fact, the
ow equations for a single FSA
typically imply fairly strong conditions on order, but the
communication equations relating the occurrence of events
in dierent FSAs do not impose strong restrictions on the
order of occurrence of events from dierent processes. To
see why, consider a system comprising two processes. The
rst process begins by trying to communicate with the second
process on channel A and then, after completing that
communication, tries to communicate with the second process
on channel B. The second process tries to complete
the communications in the reverse order. This system will
obviously deadlock, but the equations generated by INCA
would say only that the number of communications on each
channel in the rst process is equal to the number in the
second process, allowing a solution in which each communication
occurs. (This is a slight over-simplication. INCA
would actually detect the deadlock in this case, but not in
more complicated examples with several processes.) The
only mechanism INCA provides for directly constraining the
order of events in dierent processes is the use of additional
segments of the execution. While this is often enough to
eliminate solutions that do not correspond to real executions
of the system, it is expensive and restricts the range
of application of INCA. We will return to this point in the
nal section of this paper.
The second source of imprecision is the existence of cycles
in the FSAs. Consider the
ow equation for state 3 that is
shown in Figure 3. Transition 3 is a self-loop at state 3, and
ow along that transition counts both as
ow into state 3
and out of state 3. The equation x2 does not
constrain the variable x3 at all; we can simply cancel the x3
terms. Similarly, the variables x5 and x8 are not constrained
by the
ow equations in which they appear. These variables
are constrained only by the communication equation that
three of these variables are
otherwise unconstrained, this equation does not restrict the
solution set.
In fact, although the system of Figure 1 has no execution in
which a prex ending with a rendezvous at entry b contains
a rendezvous at entry a, there is a solution to the system
of equations and inequalities shown in Figure 3 with x1 ,
x2 , x5 , x7 , x8 , and x9 all equal to 1, and x3 , x4 , and x6
all equal to 0. In this solution, the requirement that the
number of rendezvous at a be at least 1 is met by setting the
unconstrained variables x5 and x8 to 1. Figure 4 shows the
FSAs with the transitions having
ow indicated by bold arcs.
The
ow in the FSA for t1 has two connected components,
one from the initial state to state 3, as expected, and one
made up of
ow in the cycle at state 4, not connected to
the
ow from state 1 to state 3. It is obvious that the
ow
in each FSA corresponding to an actual execution must be
connected, so this is a spurious solution, one that does not
correspond to a real execution.
This example illustrates the problem but is not of much
independent interest. The same problem, however, occurs
a
c
a
a
a

Figure

4: Solution with disconnected cycle
with some frequency in the analysis of more interesting sys-
tems. For instance, in our recent analysis of the Chiron
user interface development system [2], we encountered solutions
with disconnected cycles in trying to verify 2 of the 10
properties we checked. In those cases, we were able to re-formulate
the properties by specifying additional segments,
verifying other properties that allowed us to eliminate some
solutions, or choosing other events to represent the high-level
requirement. These modications, however, represent
a considerable expense in increased analyst eort and veri-
cation time. In the next section, we describe a technique for
eliminating these solutions with more than one component
of
ow in an FSA.
3. ELIMINATING SPURIOUS CYCLES
3.1 A Straightforward Approach
A related problem is well known in the optimization liter-
ature. When formulating the Traveling Salesman Problem
as an integer programming problem, it is essential to ensure
that the solution represents a single tour visiting all
the cities, rather than a collection of disconnected subtours
each visiting a proper subset of the cities. A standard approach
for eliminating solutions with disconnected subtours
is to add inequalities that prevent the solution from visiting
cities in a subset U unless the solution includes an arc
from a city not in U to one in U . Thus, if the variable x i;j
is 1 if the solution represents a tour in which the salesman
goes directly from city i to city j, and 0 otherwise, the standard
formulation of the Traveling Salesman problem would
include, for each j, the inequality
to enforce the requirement that each city is entered and left
exactly once. To eliminate the possibility of a subtour in
the subset U we would add the inequality
x i;j  1, (2)
which requires that the salesman travel from a city outside
U to a city in U . (Of course, we need an inequality like (2)
for every subset U of size at least 2 and at most N 2, where
N is the number of cities.)
In our case, to prevent a solution in which there is
ow in
a disconnected cycle C, we can add an inequality requiring
that, when there is
ow in C, there must be
ow entering
C from outside. This is a little more complicated than the
situation for the Traveling Salesman Problem. In that case,
we know by (1) that the solution must enter each city exactly
once. In our case, we do not want to require
ow into
one of the states making up C unless there is
ow along
one of the transitions in C. For instance, we only want to
require
ow on transition 4 in our example when there is
ow on transition 5. To do this in general, we would need a
quadratic inequality such as
x4x5  x5 . (3)
Integer quadratic programming is, however, much harder
than integer linear programming and we would like to avoid
introducing quadratic inequalities. The standard technique
is to impose an upper bound B on all the variables (i.e.,
to assume that no transition occurs more than B times),
and to replace the quadratic inequality (3) with the linear
inequality
The integer solutions of (3) having x4 ; x5  B are exactly
the same as those of (4). (We note that imposing an upper
bound on all the variables would mean that INCA's analysis
is no longer strictly conservative. If the system of inequalities
has no solutions with the x i all less than or equal to
B, we only know that no execution on which each transition
occurs at most B times can violate the property. Since B
can be taken to be quite large, such as 10; 000 or 100; 000,
this restriction is unlikely to be a serious one in practice.)
The problem with these approaches is that they may require
too many extra inequalities. The number of subtours that
have to be eliminated in the Traveling Salesman Problem is
essentially the number of subsets of the set of cities and is
clearly exponential in the number of cities. Similarly, the
number of cycles in an FSA can be essentially equal to the
number of subsets of its set of states. We have constructed
a small concurrent Ada program with only 90 lines of code
in which the FSA for one task has only 42 states but has
1,160,290,624 distinct subsets of states each forming at least
one cycle. An integer programming problem with that many
inequalities is infeasible. A better method is required.
3.2 A More Practical Method
In this section, we describe a method for preventing spurious
cycles that requires, for each FSA and segment of execution,
new variables and S new inequalities, where
S is the number of states in the FSA and T is the number
of transitions.
The basic idea is essentially as follows. Suppose we have a
solution to the system of equations and inequalities originally
generated by INCA. For each FSA and each segment
of execution, we attempt to construct a subgraph with the
same vertices as the FSA but whose edges are a subset of
those that have positive
ow in the solution. We require
that (i) if there is
ow into a vertex v in the solution, some
edge terminating in v must occur in the subgraph, and (ii)
each vertex v of the subgraph can be assigned a \depth" dv
in such a way that the depth of a given node is greater than
that of any of its predecessors in the subgraph.
If the original solution has no disconnected cycles, we can
choose for our subgraph a spanning tree for the edges with
ow and take the depth of a vertex to be the distance from
the root of the tree to the vertex. If the solution has a
disconnected cycle C, however, we cannot construct such
a subgraph. To see why, suppose we could construct the
subgraph, and let v be a vertex in C for which dv  du
for all u 2 C. Since there is
ow into v in the solution, v
must have some predecessor u in the subgraph. Since the
cycle C is disconnected from the
ow starting at the initial
state of the FSA, the state u must also lie in C. But if
u is a predecessor of v in the subgraph, we have dv > du ,
contradicting the minimality of dv on C.
Of course, we do not want to consider the possible solutions
to the system of equations and inequalities generated
by INCA one at a time, attempting to construct the sub-graph
separately for each solution. Instead, we add new
variables and inequalities, leading to an augmented system
of equations and inequalities whose integer solutions correspond
exactly to the integer solutions of the original system
for which the appropriate subgraph can be constructed.
We describe the procedure for generating this augmented
system for the case of a single FSA F and a single segment
of execution. For each variable x i in the original system corresponding
to a transition in F , we introduce a new variable
This variable will be 1 if the corresponding edge is in the
subgraph, and 0 otherwise.
For each state v in F , we introduce a new variable dv with
bounds
where N is some integer which is at least the maximum
length of any non-self-intersecting path through the FSA.
For instance, N can be taken to be the number of states in
F . The variable dv will be the depth of v.
We then generate inequalities involving these new variables.
Each variable s i corresponds to a transition from some state
u of F to a state v. We generate the inequalities
The rst inequality says that s i must be 0 if x i is 0, so
that the corresponding edge can be in the subgraph only if
the solution has positive
ow along that edge. The second
inequality requires that dv be greater than du if the edge
from u to v is in the subgraph. If the edge is not in the
subgraph (i.e., if s i is 0), the inequality reads dv  du N ,
and the bounds on dv and du make that vacuous.
Finally, let In(v) denote the number of transitions into the
state v. For each state v of F , other than the initial state,
we generate the inequality
where the sums are taken over all transitions into the state
and B is an upper bound on all the variables. (As noted
earlier, B can be taken to be quite large.) If all the x j
are 0, this inequality is satised vacuously, but if any x j is
positive, the inequality forces some s j to be positive. This
means that, in a solution with
ow into state v, some edge
terminating in v belongs to the subgraph.
The argument sketched at the beginning of this section proves
the following theorem, showing that this method eliminates
only solutions with disconnected cycles.
Theorem 1. Let P be the system of equations and inequalities
generated by INCA to check a particular property
of a given concurrent system. Let P 0 be the augmented system
constructed from P as described above. A solution of
assigns values to all the variables in P as well as additional
variables; we thus obtain an assignment of values to
the variables in P from a solution to P 0 by projection. The
set of integer solutions of P with all variables taking values
at most B and no disconnected cycles is exactly equal to the
set of projections of integer solutions of P 0 with all variables
taking values at most B.
In general, a query can specify more than one execution
segment, so the situation is a bit more complicated. In the
general case, INCA constructs a
owgraph as follows. First,
it creates one copy of each FSA for each segment specied in
the query. Each copy can then be optimized independently,
removing unnecessary states or transitions, based on the restrictions
imposed in the query for that segment. As seen in
the example in Section 2.1, INCA can determine from the
query the states in which each FSA could be at the end of
each segment. It then adds a \connect" edge from each of
the possible end states for segment i to the corresponding
state in segment i + 1. These edges connect the
ow representing
events in one segment of an execution to
ow in the
next segment. Finally, an initial node is added with connect
edges to certain states in the rst segment of each task,
and a nal node is added with incoming connect edges from
the possible end states in the nal segment of each task.
This
owgraph is the actual structure which INCA uses to
generate the ILP system.
The algorithm described in this section can actually be applied
to any subset of vertices in the
owgraph, rather than
to the whole
owgraph, thereby eliminating only those spurious
solutions in which there is a disconnected cycle contained
in that subset. For given a subset W of vertices of
the
owgraph, one can form a new graph V as follows. Create
a vertex in V for each vertex in W , and also add an
initial and a nal vertex to V . For each edge joining two
vertices in W , create a corresponding edge in V . For each
edge originating outside W and terminating in W , create
a corresponding edge in V from the initial vertex to the
corresponding vertex. For each edge originating in W and
terminating outside of W , create a corresponding edge in V
from the corresponding vertex to the nal vertex.
Each edge in V has associated to it an ILP variable, which
is the variable associated to the corresponding edge in the
original
owgraph. So we can apply the algorithm to V ,
generating new variables and inequalities which are added
to those INCA originally produced from the
owgraph, and
the same arguments given above go through.
Restricting the algorithm in this way has many practical ap-
plications. Suppose, for example, that a solution contains
a single disconnected cycle. It is clear that that cycle must
lie within a single segment of a single task in the
owgraph.
That is because there are no edges from a state in one segment
to a state in a preceding segment, and there are no
edges from states of one task to another. Now, to apply the
cycle-elimination algorithm to the entire
owgraph might be
very expensive, both in terms of the time and memory to
generate the new variables and constraints, and the time and
memory needed by the ILP tool to solve the new system. In
this case, it makes sense to apply the algorithm only to the
problematic segment of the problematic task. Typically, the
segments behave quite independently, and the existence of
spurious cycles in one segment is not related to the existence
of spurious cycles in other segments.
One might be tempted to be as conservative as possible and
apply the cycle-elimination algorithm to only those vertices
involved in the oending cycle. This is usually fruitless, as,
more often than not, another spurious solution will be found
by expanding the cycle to include other vertices. However,
no matter how much the cycle expands, it still must lie entirely
in the single segment of the single task, and therefore
the best strategy might be to apply the algorithm to the entire
problematic segment in that task as soon as one spurious
cycle appears there.
4. PRELIMINARY EXPERIMENTS
The current version of INCA consists of about 12,000 lines
of Common Lisp. INCA writes out a le describing the system
of equations and inequalities in a standard format (the
MPS format), and we then use a commercial package called
CPLEX to read this le and solve the system. (We also
use a separate program to translate Ada programs into the
native input language of INCA). The optimizations INCA
uses to reduce the number of variables and inequalities make
the introduction of new variables and inequalities somewhat
complicated, and integrating our method into INCA will
involve a substantial programming eort. For our initial
exploration of the eect of applying our method, we have
therefore chosen to proceed by modifying the MPS le produced
by INCA. We have written a Java program that reads
this le, and a le describing the
owgraph, and produces a
new MPS le representing the augmented system of equations
and inequalities. We can then compare the performance
of CPLEX on the original system and the augmented
system. At this stage, however, we cannot measure how long
it would take INCA to generate the augmented system of
equations and inequalities.
For these experiments, we used INCA version 3.4, Harlequin
Lispworks 4.1.0, and CPLEX version 6.5.1 on a Sun Enterprise
3500 with two processors and 2 GB of memory, running
Solaris 2.6. The upper bound B representing the maximum
number of times an edge may be traversed in a violating execution
was taken to be 10; 000. We used the default options
on CPLEX, except for the following changes: mip strategy
nodeselect was set to 2, mip strategy branch was set to 1,
and mip limits solutions was set to 1. (The rst two affect
choices made in the branch-and-bound algorithm and
the third stops the search as soon as an integer solution is
found.) For each ILP problem, we ran CPLEX ve times
and took the average time. The times reported here were
collected using the time command, and include both user
and system time.
4.1 A Scalable Version of the Example from
Section 2
For the rst experiment, we created a scalable version of the
simple example described in Section 2.1. Given an integer
we modied the Ada program in Figure 1 to have n
copies of task t2 and to have alternatives in the outer
select statement. Each of the new copies of task t2 calls
the same entries in t1. (In detail, we replaced task t2 with n
copies of itself, calling these tc1,. ,tcn. In the body of t1,
we replaced the rst accept c line with n copies of itself and
replaced the body of text beginning with the rst accept a
and ending with the last or with n copies of itself.)
As before, we wish to verify that a rendezvous at entry a can
never precede a rendezvous at entry b. INCA constructs an
FSA for t1 in which there are 2n+4 nodes and 4n 2 +3 edges.
(The picture is slightly dierent from what one might expect
because we have added a start vertex and an end vertex,
and INCA performs some trimming of the FSA.) There are
distinct subsets of the vertex set for t1 which
cycles.
For each n, INCA nds a spurious solution involving a disconnected
cycle in t1. Applying the algorithm in Section 3.2
to the portion of the
owgraph coming from the FSA for
task t1, however, yields an ILP problem that CPLEX reports
has no integer solutions, thus verifying that an a can
never precede a b.
For n  3, the number of variables in the INCA-generated
ILP system is 4n 2 +2n, and the number of constraints (equa-
tions and inequalities) is 5n+ 1. The number of variables in
the new system is
and the number of constraints is
The time that it takes CPLEX to nd a spurious solution to
the original system and the time it takes to determine the inconsistency
of the augmented system are shown in Figure 5.
These times are very modest, all under 10 seconds, and are
in fact dwarfed by the time it takes INCA to generate its
internal representations of the problem and the original ILP
system. was about 30 minutes.) It seems,
however, that for large n, the substantial increase in the
number of constraints in the augmented system, due to the
large number of edges in the FSA for t1, does begin to have
a signicant impact on the time to solve the ILP problem.13579
time
Conclusive result with cycle elimination
Spurious solution without cycle elimination

Figure

5: CPLEX times for scaled simple example
4.2 Spurious Cycles in Chiron
The second experiment involves the Chiron user interface
system [9]. A Chiron client comprises some abstract data
types to be depicted, artists that maintain mappings between
these ADTs and the visual objects appearing on the
screen, and runtime components that provide coordination.
In particular, certain events indicating changes in the state
of the ADTs are dened, and an ADT Wrapper task noties
a Dispatcher task whenever an event occurs. The Dispatcher
maintains an array for each event that records which artists
are interested in being notied of that event. (Artists register
and unregister for an event to indicate their current
interest in being notied.) After receiving the event from
the ADT Wrapper, the Dispatcher then loops through the
artists in the appropriate array and calls an entry in each
artist to notify it of the event. The Chiron architecture is
highly concurrent and even a toy Chiron interface represents
about 1000 lines of Ada code. In [2], we compared the performance
of several nite-state verication tools (FLAVERS,
INCA, SMV, and SPIN) in checking a number of properties
of a Chiron interface with two artists and n dierent kinds
of events, for n ranging from 2 to 70.
One of the properties we wish to verify about this system,
called Property 4 in [2], is that the Dispatcher noties the
artists of the right event. For example, if the Dispatcher
receives event e1 from the ADT Wrapper, we wish to show
that it does not notify any artist of event e2 until it has
notied the appropriate artists of e1. To formulate this
property as an INCA query takes 2 segments.
We were in fact able to verify this property using INCA, but
only in systems where the number of kinds of events, n, is
at most 5. (FLAVERS and SPIN were able to verify this
property up to at least
To scale the problem further with INCA, we needed to decompose
the Dispatcher task into a subsystem. This entails
creating a new task Dispatch ei, for
maintains the array for event ei. The Dispatcher task itself
is left as an interface which just passes register, unregister,
and notication requests on to the appropriate Dispatch ei
in a way such that no additional concurrency is introduced.
(If the internal communications of the Dispatcher subsystem
are hidden, the new system is observationally equivalent
to the original one.) This decomposed system has the
advantage that as n increases, the size of each Dispatch ei
FSA remains constant, although the number of these tasks
increases. While in general this decomposition greatly improves
the performance of INCA, for this property INCA
yields an inconclusive result. The problem is a disconnected
cycle in the task Dispatch e1 in the second segment.
To get around this problem, we reformulated the property
using dierent events to represent the high-level property.
This depended on the prior verication of other properties
relating the events used in the original and new formulations
and was cumbersome and time-consuming. (Once the property
was reformulated, however, the performance of INCA
on this decomposed system was considerably better than
that of the other tools. By 30, the INCA time was already
roughly an order of magnitude better than the times
for the other tools and INCA could verify the property for
much larger values of n. The dierences in performance of
the tools on this property, for the two versions of the Chiron
system, are typical of what we observed on other properties.
The implications of this are discussed in [2].)
Using the cycle elimination algorithm described here, we
were able to verify the original property directly, for 2
70. In this case there are 23 nodes and 63 edges in the
problematic task/segment for all n. Hence for each n our
algorithm adds 86 variables and 148 constraints to the ILP
system. For n  3, the number of variables in the original
system is
where (n) is 58, 118, or 84, according as n is congruent
modulo 3 to 0, 1, or 2, respectively. (This re
ects the way
we chose to have artists register for events as we scaled up
the number of events.) The number of constraints in the
augmented system is
where similarly the value of (n) is 195, 281, or 235. In this
case, eliminating spurious cycles adds a constant number
of variables and constraints as n increases. The CPLEX
times for each n, for the original system for which CPLEX
found a spurious solution and the result of the analysis was
inconclusive, and for the augmented system for which the
property was conclusively veried, are given in Figure 6.
Again, the times are all under 5 seconds and represent a
very small portion of the total analysis time. (For
70, this was about 2.5 minutes.) The spike at
the CPLEX time for the augmented system seems to be
due to the occurrence of certain numerical problems for this
particular system.
4.3 The Cost of Unnecessarily Preventing Spurious
Cycles
We also tried adding the cycle elimination variables and constraints
to a system which already yielded a conclusive re-
sult. This might yield insight into the marginal cost of having
INCA add cycle elimination by default for any problem.
For this experiment, we used another property from [2]. In135
time
events
Conclusive result with cycle elimination
Spurious solution without cycle elimination

Figure

times for Chiron Property 4
this case, we used Property 1b, which says that an artist
never unregisters for an event unless it is already registered
for that event. As in [2], we restricted ourselves to checking
this for a single artist and event. The resulting property
requires 2 segments for its formulation as an INCA query.
Using the decomposed dispatcher version of the client code,
INCA veried this property without any need for cycle elim-
ination, for n  70. The number of variables in the INCA-
generated ILP system (for n
where (n) is 77, 146, or 107 according as n is congruent
modulo 3 to 0, 1, or 2, respectively. The number of constraints
is
where similarly (n) is 69, 96, or 81.
We then applied the cycle-elimination algorithm to all of the
(recall that there is a separate Dispatch ei for
each of the n event types) and both segments. (In the experiment
discussed in the previous section, we only applied
the algorithm to one FSA and one segment.) This entailed
adding
new variables to the system, where (n) is 552, 833, or 682,
and adding
new constraints, where (n) is 897, 1391, or 1123. The times
required by CPLEX to nd the conclusive result in each case
are graphed in Figure 7.
Although the ILP systems in the augmented case are quite
large (18,087 variables and 22,563 constraints for
the larger n, it still appears that CPLEX can determine the
inconsistency of the system in a very short time (less than
4 seconds). If this example is typical, the real cost in introducing
cycle elimination in INCA might lie in generating
the new ILP system, not in solving it.
5. CONCLUSIONS AND FUTURE WORK
time
events
Conclusive result with cycle elimination
Conclusive result without cycle elimination

Figure

7: CPLEX times for Chiron Property 1b
Some nite-state verication tools always provide a conclusive
result on any problem they can analyze. A tool that
walks a graph of the reachable states of a concurrent system
will never report that the system might deadlock when in
fact the system is deadlock-free (assuming, of course, that
the graph correctly represents the reachable state space of
the system). But such a tool must be able to store the full
set of reachable states, and is unable to report any results
for a system whose reachable state space exceeds the storage
available. Other tools, such as INCA, deliberately overestimate
the collection of possible executions of the system, and
thus accept the possibility of inconclusive results (or spurious
reports of the possible faults), in order to increase the
range of systems to which they can be applied.
For INCA, there are two main sources of imprecision in the
representation of executions of the system. The rst of these
is the fact that semantic restrictions on the order of occurrence
of events in dierent concurrent processes are generally
not represented in the equations and inequalities used
by INCA. The second source of imprecision is the fact that
the equations and inequalities allow solutions in which the
ow in the FSA representing a concurrent process may have
cycles not connected to the initial state. In this paper, we
have shown how imprecision caused by this second source
may be eliminated.
Specic cases of inconclusive results can often be addressed
by careful reformulation of the property being checked, although
this may require the verication of additional properties
to justify the reformulation. This process can require
very substantial amounts of eort on the part of the human
analysts, as well as considerable costs to carry out the necessary
verications. We have also sometimes addressed inconclusive
results by manually inserting special inequalities
to prevent disconnected
ow on a small number of specic
cycles. The problem with generalizing this approach is that
the number of cycles may well be exponential in the size
of the concurrent system, and each of the cycles requires a
separate inequality. Even if it were feasible to automate the
generation of these inequalities, the resulting ILP problems
would be far too large to solve. The numbers of new variables
and inequalities introduced by the method presented in
this paper are linear in the number of states and transitions
in the FSAs representing the processes of the concurrent
system being analyzed.
We have reported here the results of some preliminary experiments
aimed at assessing the cost, in increased time to
solve the systems of equations and inequalities, of applying
our method. These experiments suggest that the cost
is relatively small, especially when the eort of the human
analysts is taken into account. We plan to carry out additional
experiments of the same type, and to integrate our
technique into the INCA toolset so that we can also evaluate
the time needed to generate the additional variables and
inequalities.
We are also investigating approaches to eliminating some of
the imprecision caused by not representing restrictions on
the order of events in dierent processes. Fully representing
the restrictions imposed by the semantics of the programming
language or design notation may not be practical and
might limit the applicability of INCA in the same way that
having to store the full set of reachable states limits the
applicability of tools based on exploring the graph of reachable
states. We are therefore exploring methods that allow
the analyst to control the degree to which restrictions on
order are represented. For example, one approach that we
are considering is to formulate some of the
ow and communication
equations in such a way that they hold at every
stage of an execution, not just the end. These reformulated
ow and communication equations therefore enforce some of
the restrictions on the order of events in dierent processes.
They also determine a region in n-dimensional Euclidean
space, where n is the number of variables in the system of
equations and inequalities. We then look for a point satisfying
the full system of equations and inequalities that can
be reached by taking certain integer-sized steps through this
region. Successfully reducing this kind of imprecision will be
important in applying the INCA approach to many systems
where interprocess communication is only through access to
shared data.
6.



--R

Automated derivation of time bounds in uniprocessor concurrent systems.

An empirical comparison of static concurrency analysis techniques.
An empirical evaluation of three methods for deadlock analysis of Ada tasking
Evaluating deadlock detection methods for concurrent software.
A practical method for bounding the time between events in concurrent real-time systems
Towards scalable compositional analysis.
Using integer programming to verify general safety and liveness properties.

--TR
A practical technique for bounding the time between events in concurrent real-time systems
An empirical evaluation of three methods for deadlock analysis of Ada tasking programs
Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems
Towards scalable compositional analysis
Using integer programming to verify general safety and liveness properties
Evaluating Deadlock Detection Methods for Concurrent Software
Comparing Finite-State Verification Techniques for Concurrent Software
INCA;integer programming;finite-state verification;cycles