Sharon Shoham
Skip Abstract Section
Skip Supplemental Material SectionAbstract
This work exploits and extends the game-based framework of CTL model checking for counterexample and incremental abstraction-refinement. We define a game-based CTL model checking for abstract models over the 3-valued semantics, which can be used for verification as well as refutation. The model checking process of an abstract model may end with an indefinite result, in which case we suggest a new notion of refinement, which eliminates indefinite results of the model checking. This provides an iterative abstraction-refinement framework. This framework is enhanced by an incremental algorithm, where refinement is applied only where indefinite results exist and definite results from prior iterations are used within the model checking algorithm. We also define the notion of annotated counterexamples, which are sufficient and minimal counterexamples for full CTL. We present an algorithm that uses the game board of the model checking game to derive an annotated counterexample in case the examined system model refutes the checked formula.
Supplemental Material
Available for Download
pdf
a1-shoham-apndx.pdf (137.4 KB)
Online appendix to designing mediation for context-aware applications. The appendix supports the information on article 1.
- Asteroth, A., Baier, C., and Assmann, U. 2001. Model checking with formula-dependent abstract models. In Proceedings of the International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2102, 155--168. Google Scholar
Digital Library
- Barner, S., Geist, D., and Gringauze, A. 2002. Symbolic localization reduction with reconstruction layering and backtracking. In Proceedings of the International Conference on Computer-Aided Verification (CAV). Copenhagen, Denmark. Google ScholarDigital Library
- Bollig, B., Leucker, M., and Weber, M. 2002. Local parallel model checking for the alternation-free mu-calculus. In Proceedings of the 9th International SPIN Workshop on Model Checking of Software. Springer-Verlag Inc. Google ScholarDigital Library
- Bruns, G. and Godefroid, P. 1999. Model checking partial state spaces with 3-valued temporal logics. In Proceedings of the International Conference on Computer-Aided Verification. 274--287. Google ScholarDigital Library
- Bruns, G. and Godefroid, P. 2000. Generalized model checking: Reasoning about partial state spaces. In Proceedings of the International Conference on Concurrency Theory (CONCUR'00). Lecture Notes in Computer Science, vol. 1877, 168--182. Google ScholarDigital Library
- Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., and D.Wang. 2002. Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD). Google ScholarDigital Library
- Chechik, M., Devereux, B., and Easterbrook, S. 2001. Implementing a multi-valued symbolic model checker. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 404--419. Google ScholarDigital Library
- Chechik, M., Gurfinkel, A., and Devereux, B. 2002. chi-chek: A multivalued model-checker. In Proceedings of the International Conference on Computer-Aided Verification (CAV). 505--509. Google ScholarDigital Library
- Clarke, E. and Emerson, E. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the Workshop on Logics of Programs, vol. 131, Lecture Notes in Computer Science, Springer-Verlag, Berlin, 52--71. Google ScholarDigital Library
- Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-guided abstraction refinement. In Proceedings of the 12th International Conference on Computer-Aided Verification (CAV). Google ScholarDigital Library
- Clarke, E., Grumberg, O., McMillan, K., and Zhao, X. 1995. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the 32nd Design Automation Conference (DAC). IEEE Computer Society Press. Google ScholarDigital Library
- Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press. Google ScholarDigital Library
- Clarke, E., Gupta, A., Kukula, J., and Strichman, O. 2002. SAT based abstraction-refinement using ILP and machine leraning techniques. In Proceedings of the International Conference on Computer-Aided Verification (CAV). Copenhagen, Denmark. Google ScholarDigital Library
- Clarke, E., Jha, S., Lu, Y., and Veith, H. 2002. Tree-like counterexamples in model checking. In Proceedings of the 17th Annual IEEE Symposium on Logic In Computer Science (LICS). Copenhagen, Denmark. Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). Los Angeles, CA, 238--252. Google ScholarDigital Library
- Dams, D., Gerth, R., and Grumberg, O. 1997. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19, 2 (March). Google ScholarDigital Library
- Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the Conference on Computer-Aided Verification. 160--171. Google ScholarDigital Library
- Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., and Campenhout, D. V. 2003. Reasoning with temporal logic on truncated paths. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2725. Springer, 27--39.Google Scholar
- Emerson, E. and Clarke, E. 1982. Using branching time logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241--266.Google ScholarCross Ref
- Godefroid, P., Huth, M., and Jagadeesan, R. 2001. Abstraction-based model checking using modal transition systems. In Proceedings of International Conference on Concurrency Theory (CONCUR'01). Google ScholarDigital Library
- Godefroid, P. and Jagadeesan, R. 2002. Automatic abstraction using generalized model checking. In Proceedings of the Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2404. Springer Verlag, 137--150. Google ScholarDigital Library
- Godefroid, P. and Jagadeesan, R. 2003. On the expressiveness of 3-valued models. In Proceedings of the 4th Conference on Verification, Model Checking and Abstract Interpretation (VMCA). Lecture Notes in Computer Science, vol. 2575. Springer-Verlag, 206--222. Google ScholarDigital Library
- Govindaraju, S. and Dill, D. 1998. Verification by approximate forward and backward reachability. In Proceedings of the International Conference on Computer-Aided Design. 366--370. Google ScholarDigital Library
- Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, 72--83. Google ScholarDigital Library
- Gurfinkel, A. and Chechik, M. 2003a. Generating counterexamples for multivalued model-checking. In Proceedings of the IEEE International Symposium on Formal Methods Europe (FME'03). 503--521.Google Scholar
- Gurfinkel, A. and Chechik, M. 2003b. Proof-like counter-examples. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03).Google Scholar
- Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, Portland, Oregon, 58--70. Google ScholarDigital Library
- Huth, M., Jagadeesan, R., and Schmidt, D. 2001. Modal transition systems: A foundation for three-valued program analysis. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 2028, 155--169. Google ScholarDigital Library
- Kupferman, O., Vardi, M., and Wolper, P. 2000. An automata-theoretic approach to branching-time model checking. J. ACM 47, 2, 312--360. Google ScholarDigital Library
- Kurshan, R. 1994. Computer-Aided-Verification of Coordinating Processes. Princeton University Press. Google ScholarDigital Library
- Larsen, K. and Thomsen, B. 1988. A modal process logic. In Proceedings of 3rd Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, 203--210.Google Scholar
- Larsen, K. G. 1989. Modal specifications. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems. Grenoble, France. J. Sifakis, Ed. Lecture Notes in Computer Science, vol. 407. Springer-Verlag. Google ScholarDigital Library
- Lee, W., Pardo, A., Jang, J., Hachtel, G., and Somenzi, F. 1996. Tearing based automatic abstraction for CTL model checking. In Proceedings of the International Conference on Computer-Aided Design (ICCAD). 76--81. Google ScholarDigital Library
- Leucker, M. 1999. Model checking games for the alternation free mu-calculus and alternating automata. In Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR99). Google ScholarDigital Library
- Lichtenstein, O. and Pnueli, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages. 97--107. Google ScholarDigital Library
- Lind-Nielsen, J. and Andersen, H. 1999. Stepwise CTL model checking of state/event systems. In Computer Aided Verification. 316--327. Google ScholarDigital Library
- Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., and Bensalem, S. 1995. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6, 11--45. Google ScholarDigital Library
- Namjoshi, K. 2001. Certifying model checkers. In Proceedings of the 13th Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2102. Springer-Verlag. Google ScholarDigital Library
- Namjoshi, K. and Kurshan, R. 2000. Syntactic program transformations for automatic abstraction. In Proceedings of Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855. Springer, 435--449. Google ScholarDigital Library
- Pardo, A. and Hachtel, G. 1997. Automatic abstraction techniques for propositional mucalculus model checking. In Computer Aided Verification. 12--23. Google ScholarDigital Library
- Pardo, A. and Hachtel, G. 1998. Incremental CTL model checking using BDD subsetting. In Proceedings of the Design Automation Conference. 457--462. Google ScholarDigital Library
- Quielle, J. and Sifakis, J. 1982. Specification and verification of concurrent systems in CESAR. In Proceedings of the International Symposium on Programming. Lecture Notes in Computer Science, vol. 137. Springer Verlag, 337--351. Google ScholarDigital Library
- Saidi, H. 2000. Model checking guided abstraction and analysis. In Proceedings of the 7th International Static Analysis Symposium (SAS). Santa Barbara, CA. Google ScholarDigital Library
- Saidi, H. and Shankar, N. 1999. Abstract and model check while you prove. In Proceedings of the 11th International Conference on Computer-Aided Verification (CAV). Trento, Italy. Google ScholarDigital Library
- Shoham, S. 2003. A game-based framework for CTL counterexamples and abstraction-refinement. M.S. thesis, Department of Computer Science, Technion---Israel Institute of Technology.Google Scholar
- Stirling, C. 2001. Modal and Temporal Properties of Processes. Springer-Verlag. Google ScholarDigital Library
- Tan, L. and Cleaveland, R. 2002. Evidence-based model checking. In Proceedings of the 14th Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2404. Springer Verlag, 455--470. Google ScholarDigital Library
Index Terms
- A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
Recommendations
A counterexample-guided abstraction-refinement framework for markov decision processes
The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of counterexample guided abstraction refinement (CEGAR), wherein one ...
Relating counterexamples to test cases in CTL model checking specifications
A-MOST '07: Proceedings of the 3rd international workshop on Advances in model-based testingCounterexamples produced by model checkers are frequently exploited for the purpose of testing. Counterexamples and test cases are generally treated as essentially the same thing, while in fact they can differ significantly. For example, it might take ...
Structured Counterexamples for the Temporal Description Logic ALCCTL
SEFM '10: Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal MethodsA new algorithm for generating counterexamples for the temporal description logic ALCCTL is presented. ALCCTL is a decidable combination of the description logic ALC and computation tree logic CTL. It extends CTL by first order quantified expressions ...
Comments