Tevfik Bultan
ABSTRACT
Many concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using model checking. In this approach an abstract, finite-state model of the system is constructed; then an automatic check is made to ensure that the requirements are satisfied by the model. In practice, however, this method is limited by the state space explosion problem.We have developed a compositional method that directly addresses this problem in the context of multi-tasking programs. Our solution depends on three key space-saving ingredients: (1) checking for counter-examples, which leads to simpler search algorithms; (2) automatic extraction of interfaces, which allows a refinement of the finite model --- even before its communicating partners have been compiled; and (3) using propositional "strengthening assertions" for the sole purpose of reducing state space.In this paper we present our compositional approach, and describe the software tools that support it.
- 1.R. Alur, C. Courcoubetis, T. A. Henzinger, and P. Ho. Hybrid automata' an algomthmic approach to the specification and verification of hybrid systems. Proceed,rigs of the Workshop on Theory of Hybrid Systems, 1992. Google Scholar
Digital Library
- 2.J. 1%. Burch, E. M. Clarke, K. L. McMillan, D. L Dill, and L H Hwang. Symbolic model checking: 1020 states and beyond. Proceedings of the F~fth Annual Sympos,um on Logzc ,n Computer Science, 428-439, 1990.Google Scholar
- 3.M. Chiodo, T. R. Shlple, A. Sangiovanni-Vmcentelli, and R.K.Brayton Automatic reduction in CTL compositional model checking Proceedings CA V'92, LNCS 663, 234-247, June 1992. Google ScholarDigital Library
- 4.E M Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic spectfications. ACM Transactzons on Prograramzng Languages and Systems, 8(2):244-263, April 1986 Google ScholarDigital Library
- 5.S C. Cheung and J. Kramer. Enhancing Compositional Reachabihty Analysis with Context Constraints. Proceed,rigs FSE'93, ACM SIGSOFT, 115-125, December 1993. Google ScholarDigital Library
- 6.R Cleaveland Tableau-based model checking in the propomtional mu-calculus. Acta Informat,ca, 27:725-747, 1990. Google ScholarDigital Library
- 7.R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench. Proceed,ngs of the Workshop on Automat, c Verification Methods for Finite-State Systems, LNCS 4{07, 24-37, 1990. Google ScholarDigital Library
- 8.E. M. Clarke, D. E. Long, and K. L McMillan. Compositional model checking. Proceedings of the Fourth Annual Symposmm on Logic in Computer Science, 464-475, June 1989. Google ScholarDigital Library
- 9.E. A. Emerson and J. Y. Halpern. 'Sometimes' and 'not never' revisited, on branching versus linear time temporal logic. Journal of the A CM, 33(1):151-178, January 1986. Google ScholarDigital Library
- 10.E. A. Emerson and C Lei. Efficient model checking m fragments of the propositional mu-calculus. Proceedings of Symposium on Log,c ~n Computer Science, 267-278, 1986Google Scholar
- 11.J. Fischer and R Gerber. Compositional Model Checking of Ada Tasking Programs Proceedings COMPASS'9~i. 1994.Google ScholarDigital Library
- 12.N. Halbwachs. Delay analysis in synchronous programs CAV93, LNCS 697. 1993. Google ScholarDigital Library
- 13.R. J van Glabbeek. The linear time - branching time spectrum CONCUR90, LNCS ,t58, 1990. Google ScholarDigital Library
- 14.R. Gerber and I Lee. A Layered Approach to Automating the Verification of 1%eat-Time Systems. IEEE Trans. on Software Eng., 18(9).768-784, 1992. Google ScholarDigital Library
- 15.O. Lichtenstein and A. PnueIi Checking that finite state concurrent programs satmfy their hnear specifications. 1984.Google Scholar
- 16.J. S. Ostroff. Survey of formal methods for the spec~ficat,on and design of real-t,me systems. Draft for IEEE Press book "Tutorial on Specification of Time", 1992.Google Scholar
- 17.C. Stirling and D. Walker. CCS, hveness, and local model checking in the linear time mu-calculus. Automatic Vergficat~on Methods for F, ngte State Systems, LNCS ,107, 1989 Google ScholarDigital Library
- 18.W. J Yeh and M. Young. Compositional Reachability Analysis Using Process Algebra. Proceedings TA V4, A CM SIGSOFT, 49-59, October 1991. Google ScholarDigital Library
Index Terms
- Compositional verification by model checking for counter-examples
Recommendations
Compositional verification by model checking for counter-examples
Many concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using model checking. In this approach an abstract, finite-state model of ...
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs
TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of SystemsDespite recent advances in model checking and in adapting model checking techniques to software, the state explosion problem remains a major hurdle in applying model checking to software. Recent work in automated program abstraction has shown promise as ...
Finding feasible abstract counter-examples
A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the high-computational cost of model checking most researchers advocate the use of aggressive property-...
Comments