Abstract
Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that recent trends in both the requirements for software systems and the processes by which systems are developed suggest that domain-specific model checking engines may be more effective than general purpose model checking tools. To overcome limitations of existing tools which tend to be monolithic and non-extensible, we have developed an extensible and customizable model checking framework called Bogor. In this tool paper, we summarize (a) Bogor’s direct support for modeling object-oriented designs and implementations, (b) its facilities for extending and customizing its modeling language and algorithms to create domain-specific model checking engines, and (c) pedagogical materials that we have developed to describe the construction of model checking tools built on top of the Bogor infrastructure.
This work was supported in part by a 2004 IBM Eclipse Innovation Grant, by the U.S. Army Research Office (DAAD190110564), by DARPA/IXO’s PCES program (AFRL Contract F33615-00-C-3044), and by NSF (CCR-0306607, CCF-0429149, CCF-04444167).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bosnacki, D., Dams, D., Holenderski, L.: Symmetric SPIN. International Journal on Software Tools for Technology Transfer 4(1), 92–106 (2002)
Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder – a second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)
Chan, W., Anderson, R.J., Beame, P., Notkin, D., Jones, D.H., Warner, W.E.: Optimizing symbolic model checking for statecharts. IEEE Transactions on Software Engineering 27(2), 170–190 (2001)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Deng, W., Dwyer, M., Hatcliff, J., Jung, G.: Model-checking middleware-based event-driven real-time embedded software. In: Proceedings of the 1st Internatiuonal Symposium on Formal Methods for Component and Objects, pp. 154–181 (2002)
Dwyer, M.B., Hatcliff, J., Robby, Prasad, V.R.: Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Formal Methods in System Design 25(2-3), 199–240 (2004)
Dwyer, M.B.: Space reductions for model checking quasi-cyclic systems. In: Proceedings of the Third International Conference on Embedded Software, pp. 173–189 (2003)
Dwyer, M.B.: Analyzing interaction orderings with model checking. In: Proceedings of the 19th IEEE Conference on Automated Software Engineering, pp. 154–163 (2004)
Hatcliff, J., Deng, W., Dwyer, M., Jung, G., Prasad, V.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: Proceedings of the 25th International Conference on Software Engineering, pp. 160–173 (2003)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–294 (1997)
Hatcliff, J., Robby, Dwyer, M.B.: Verifying atomicity specifications for concurrent object-oriented software using model-checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 175–190. Springer, Heidelberg (2004)
Iosif, R.: Symmetry reduction criteria for software model checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 22–41. Springer, Heidelberg (2002)
SAnToS Laboratory. Bogor website (2003), http://bogor.projects.cis.ksu.edu
SAnToS Laboratory. Software Model Checking course materials website (2004), http://model-checking.courses.projects.cis.ksu.edu
Robby, M.B.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 267–276 (2003)
Robby, M.B., Dwyer, J.: Space-reduction strategies for model checking dynamic software. In: Proceedings of the 2nd Workshop on Software Model Chekcing. Electronic Notes in Theoritical Computer Science, vol. 89(3) (2003)
Robby, E., Rodríguez, M.B.: Checking strong specifications using an extensible software model checking framework. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 404–420. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dwyer, M.B., Hatcliff, J., Hoosier, M., Robby (2005). Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_15
Download citation
DOI: https://doi.org/10.1007/11513988_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)