Home > Static Analysis > INCA
Static Analysis
FLAVERS
PROPEL
Finite-State Verification
Property Specification
Fault-Tree Analysis
Failure Mode and Effect Analysis
MPI Verification
INCA »
Experimentation
Publications
Additional Information
All INCA Publications

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:

Using Integer Programming to Verify General Safety and Liveness Properties
James C. Corbett, George S. Avrunin, Formal Methods in System Design, 6:97-123, January 1995. (INCA-1995)

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:

 1999

Comparing Finite-State Verification Techniques for Concurrent Software
George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Pasareanu, Stephen F. Siegel, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, November 1999. (UM-CS-1999-069)

[ PostScript ] [ PDF ]

 1997

Applying Static Analysis to Software Architectures
Gleb Naumovich, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 5) and the 6th European Software Engineering Conference (ESEC 1997), Zurich, Switzerland, Springer Verlag Lecture Notes In Computer Science #1301, pp. 77-93, Sept. 1997. (UM-CS-1997-008)

[ PostScript ] [ PDF ]

 1994

Towards Scalable Compositional Analysis
James C. Corbett, George S. Avrunin, Second ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 53-61, New Orleans, December 1994. ACM Press (Appeared in Software Engineering Notes, 19(5)). (INCA-1994-A)

Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems
George S. Avrunin, James C. Corbett, Laura K. Dillon, Jack C. Wileden, IEEE Transactions on Software Engineering, 20(9):708-719, September 1994. (INCA-1994-B)

 1993

A Practical Technique for Bounding the Time Between Events in Concurrent Real-Time Systems
James C. Corbett, George S. Avrunin, ACM SIGSOFT 1993 International Symposium on Software Testing and Analysis (ISSTA 1993), Cambridge, MA, pp. 110-116, June 1993. (UM-CS-1993-CA)

[ PDF ]

 1991

Automated Analysis of Concurrent Systems with the Constrained Expression Toolset
George S. Avrunin, Ugo A. Buy, James C. Corbett, Laura K. Dillon, Jack C. Wileden, IEEE Transactions on Software Engineering, 17(11), pp. 1204-1222, November 1991. (UM-CS-1990-116)

[ Compressed PostScript ] [ PDF ]

 

This site is maintained by the Laboratory for Advanced Software Engineering Research.
© 2006 University of Massachusetts AmherstSite Policies