Improving the precision of INCA by preventing spurious cycles

ABSTRACT

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.

REFERENCES

• 1: George S. Avrunin , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.708-719, September 1994 [doi>10.1109/32.317429]
• 2: G. S. Avrunin , J. C. Corbett , M. B. Dwyer , C. S. Pasareanu , S. F. Siegel, Comparing Finite-State Verification Techniques for Concurrent Software, University of Massachusetts, Amherst, MA, 1999
• 3: A. T. Chamillard, L. A. Clarke, and G. S. Avrunin. An empirical comparison of static concurrency analysis techniques. Technical Report 96-84, Department of Computer Science, University of Massachusetts, 1996. Revised May 1997.
• 4: James C. Corbett, An empirical evaluation of three methods for deadlock analysis of Ada tasking programs, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.204-215, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187206]
• 5: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 6: J. Corbett , G. Avrunin, A practical technique for bounding the time between events in concurrent real-time systems, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.110-116, June 28-30, 1993, Cambridge, Massachusetts, United States
• 7: James C. Corbett , George S. Avrunin, Towards scalable compositional analysis, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.53-61, December 06-09, 1994, New Orleans, Louisiana, United States
• 8: James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
• 9: K. Forester, C. MacFarlane, M. Cameron, and G. Bolcer. Chiron-1 user manual. Arcadia Document UCI-93-07, University of California, Irvine, Sept. 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Design, Experimentation, Performance, Reliability, Theory, Verification

Keywords:
INCA, cycles, finite-state verification, integer programming