Inequality Necessary Conditions Analysis
Regarding a concurrent system as a collection of communicating processes,
INCA generates inequalities reflecting the numbers of times events
occur in each of those processes in an execution that violates the
property to be checked. Standard integer linear programming techniques
are then used to check the resulting system of inequalities for consistency.
If the inequalities are inconsistent, no such execution can exist and
the property is verified; if they are consistent, the solutions can
be used to guide a search for an execution that actually violates the
property and displays a corresponding fault. INCA has been successfully
applied to some very large systems, and can also be used to check timing
properties of real-time systems.
If the component processes of a concurrent system are regarded as
independent entities, we can regard an execution of the complete system
as being built up from a collection of executions of its processes
that satisfy certain compatibility conditions. For instance, when combining
executions of two communicating processes, we must ensure that the
two processes agree on the number and order of their communications.
To test whether all executions of the concurrent system satisfy some
property, we could attempt to find a compatible collection of executions
of the component processes that lead to a violation of the property.
If such a collection does not exist, then we know that every execution
of the concurrent system satisfies the property.
Checking for the existence of such a collection is, in general, an
intractable problem. INCA's approach describes weaker compatibility
conditions that must be satisfied if such a collection of process executions
exists, and checks whether those weaker conditions are consistent.
If they are not consistent, no compatible collection of process executions
can exist and we know that no execution of the concurrent system can
violate the property. If the weaker conditions are consistent, however,
we do not know that the concurrent system can violate the property
-- it might be that the real compatibility conditions cannot be satisfied
in a way that violates the property and the method would incorrectly
report that a violation could occur. The idea is to allow some inconclusive
results in order to improve tractability (analysis methods that produce
definitive results in principle but are not feasible in practice are
also inconclusive in an essential way, of course). The important thing
to note is that, as with the flow analysis, INCA will not falsely report
that the property holds for all executions of the system.
In INCA, the individual processes are regarded as finite state automata,
and the necessary conditions are expressed as linear inequalities on
the occurrences of transitions in those automata. The consistency of
the set of linear inequalities is checked using standard integer linear
programming techniques. The approach is inherently compositional, in
the sense that the inquealities are generated from the automata corresponding
to the individual processes, and avoids enumerating the states of the
full concurrent system. The INCA method has been implemented in a set
of tools that can check both safety and liveness properties of concurrent
systems specified in an Ada-like design language, and has been successfully
used with systems having more than 10500 states. The method has also
been applied to analyze timing properties of real-time concurrent systems
and to check the equivalence of subsystems in a compositional analysis
. It has also been used to check application-specific properties of
software architectures.
Selected Publications
This is the best single reference on the INCA approach:
[an error occurred while processing this directive]
These papers compare INCA to other finite-state verification tools
and show how it can be applied to particular types of systems, including real-time systems:
[an error occurred while processing this directive]
This site is maintained by the