|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| S.F. Siegel, G.S. Avrunin, "Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles," IEEE Transactions on Software Engineering, vol. 28, no. 2, pp. 115-128, February, 2002. | |||
| BibTex | x | ||
| @article{ 10.1109/32.988494, author = {S.F. Siegel and G.S. Avrunin}, title = {Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles}, journal ={IEEE Transactions on Software Engineering}, volume = {28}, number = {2}, issn = {0098-5589}, year = {2002}, pages = {115-128}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.988494}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - JOUR JO - IEEE Transactions on Software Engineering TI - Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles IS - 2 SN - 0098-5589 SP115 EP128 EPD - 115-128 A1 - S.F. Siegel, A1 - G.S. Avrunin, PY - 2002 KW - INCA KW - finite-state verification KW - cycles KW - integer programming. VL - 28 JA - IEEE Transactions on Software Engineering ER - | |||
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.
[1] J.C. Corbett and G.S. Avrunin, "Using Integer Programming to Verify General Safety and Liveness Properties," Formal Methods in System Design, vol. 6, pp. 97-123, Jan. 1995.
[2] Specification patterns web site.http://www.cis.ksu.edu/santosspec-patterns /. 2000.
[3] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, “Patterns in Property Specifications for Finite-State Verification,” Proc. 21st Int'l Conf. Software Eng., pp. 411–420, May 1999.
[4] G.S. Avrunin, J.C. Corbett, M.B. Dwyer, C.S. Pasareanu, and S.F. Siegel, ”Comparing Finite-State Verification Techniques for Concurrent Software,” Technical Report UM-CS-1999-069, Dept. of Computer Science, Univ. of Massachusetts, Amherst, Nov. 1999.
[5] A.T. Chamillard, L.A. Clarke, and G.S. Avrunin, “An Empirical Comparison of Static Concurrency Analysis Techniques,” Technical Report 96-84, Dept. of Computer Science, Univ. of Massachusetts, Amherst, 1996, revised, May 1997.
[6] J.C. Corbett, "An Empirical Evaluation of Three Methods for Deadlock Analysis of Ada Tasking Programs," Software Eng. Notes, pp. 204-215, Proc. Int'l Symp. Software Testing and Analysis, Aug. 1994
[7] J.C. Corbett, “Evaluating Deadlock Detection Methods for Concurrent Software,” IEEE Trans. Software Eng., vol. 22, no. 3, pp. 161–179, Mar. 1996.
[8] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[9] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[10] J.C. Corbett and G.S. Avrunin, "A Practical Method for Bounding the Time Between Events in Concurrent Real-Time Systems," Proc. Int'l Symp. Software Testing and Analysis (ISSTA), Ostrand and Weyuker [37], New York: ACM Press, pp. 110-116, June 1993.
[11] G.S. Avrunin, J.C. Corbett, L.K. Dillon, and J.C. Wileden, Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems IEEE Trans. Software Eng., vol. 20, no. 9, 1994.
[12] J.C. Corbett and G.S. Avrunin, “Towards Scalable Compositional Analysis,” in Wile [26], pp. 53–61, Dec. 1994.
[13] K. Forester, C. MacFarlane, M. Cameron, and G. Bolcer, “Chiron-1 User Manual,” Arcadia Document UCI-93-07, Univ. of California, Irvine, Sept. 1993.
[14] M.B. Dwyer and L.A. Clarke, "Data Flow Analysis for Verifying Properties of Concurrent Programs," Software Eng. Notes, vol. 19, no. 5, pp. 62-75, Proc. ACM SIGSOFT Symp. Foundations of Software Eng., Dec. 1994.
[15] E.M. Clarke Jr., O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 2000.
[16] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
[17] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[18] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng, “Bandera: Extracting Finite-State Models from Java Source Code,” Proc. 22nd Int'l Conf. Software Eng., pp. 439–448, June 2000.
[19] M.B. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, and H. Zheng, “Tool-Supported Program Abstraction for Finite-State Verification,” Proc. 23rd Int'l Conf. Software Eng., pp. 177–187, May 2001.
[20] R.N. Taylor, “Complexity of Analyzing the Synchronization Structure of Concurrent Programs,” Acta Informatica, vol. 19, pp. 57–84, 1983.
[21] J. Reif and S. Smolka, “The Complexity of Reachability in Distributed Communicating Processes,” Acta Informatica, vol. 25, no. 3, pp. 333–354, 1988.
[22] R.H.B. Netzer and B.P. Miller, “On the Complexity of Event Ordering for Shared-Memory Parallel Program Executions,” Proc. Int'l Conf. Parallel Processing, pp. II–93–II–97, Aug. 1990.
[23] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[24] T. Murata, B. Shenker, and S.M. Shatz, "Detection of Ada Static Deadlocks Using Petri Net Invariants," IEEE Trans. Software Eng., vol. 15, no. 3, pp. 314-326, Mar. 1989.
[25] J. Esparza and S. Melzer, “Verification of Safety Properties Using Integer Programming: Beyond the State Equation,” Formal Methods in System Design, vol. 16, pp. 159–189, 2000.
[26] D. Wile, ed., Proc. Second ACM SIGSOFT Symp. Foundations of Software Eng., Dec. 1994.