Abstract
Explicit-State Model Checking is a well-studied technique for the verification of concurrent programs. Due to exponential costs associated with model checking, researchers often focus on applying model checking to software units rather than whole programs. Recently, we have introduced a framework that allows developers to specify and model check rich properties of Java software units using the Java Modeling Language (JML). An often overlooked problem in research on model checking software units is the problem of environment generation: how does one develop code for a test harness (representing the behaviors of contexts in which a unit may eventually be deployed) for the purpose of driving the unit being checked along relevant execution paths?
In this paper, we build on previous work in the testing community and we focus on the use of coverage information to assess the appropriateness of environments and to guide the design/modification of environments for model checking software units. A novel aspect of our work is the inclusion of specification coverage of JML specifications in addition to code coverage in an approach for assessing the quality of both environments and specifications. To study these ideas, we have built a framework called MAnTA on top of the Bogor Software Model Checking Framework that allows the integration of a variety of coverage analyses with the model checking process. We show how we have used this framework to add two different types of coverage analysis to our model checker (Bogor) and how it helped us find coverage holes in several examples. We make an initial effort to describe a methodology for using code and specification coverage to aid in the development of appropriate environments and JML specifications for model checking Java units.
This work was supported in part by the U.S. Army Research Office (DAAD190110564), by DARPA/IXO’s PCES program (AFRL Contract F33615-00-C-3044), by NSF (CCR-0306607), by Lockheed Martin, and by Rockwell-Collins.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Rajamani, S.K.: The slam toolkit. In: Proceedings of the 13th International Conference on Computer Aided Verification, pp. 260–264. Springer, Heidelberg (2001)
Binder, R.V.: Testing object-oriented systems: models, patterns, and tools. Addison-Wesley, Longman Publishing Co., Inc. (1999)
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)
Chockler, H., Kupferman, O., Kurshan, R., Vardi, M.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 66–78. Springer, Heidelberg (2001)
Dwyer, M.B., Hatcliff, J., Prasad, V.R., Robby: Exploiting object escape and locking information in partial order reductions for concurrent object-oriented programs. Formal Methods in System Designs (2004) (to appear)
Dwyer, M.B., Hatcliff, J., Schmidt, D.: Bandera: Tools for automated reasoning about software system behaviour. ERCIM News 36 (January 1999)
Engler, D.R., Musuvathi, M.: Static analysis versus software model checking for bug finding. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 191–210. Springer, Heidelberg (2004)
Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley Pub. Co., Reading (1995)
Groce, A., Visser, W.: Model checking java programs using structural heuristics. In: Proceedings of the International Symposium on Software Testing and Analysis, pp. 12–21. ACM Press, New York (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pp. 58–70 (January 2002)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–294 (1997)
Holzmann, G.J., Smith, M.H.: A practical method for verifying event-driven software. In: Proceedings of the 21st international conference on Software engineering, pp. 597–607. IEEE Computer Society Press, Los Alamitos (1999)
Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proceedings of the 36th ACM/IEEE Design automation conference, pp. 300–305. ACM Press, New York (1999)
Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 82–98. Springer, Heidelberg (1999)
Lea, D.: Concurrent Programming in Java, 2nd edn. Addison-Wesley, Reading (2000)
Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modeling language. In: Formal Underpinnings of Java Workshop (October 1998)
Musuvathi, M., Engler, D.R.: Model checking large network protocol implementations. In: Proceedings of The First Symposium on Networked Systems Design and Implementation, pp. 155–168. USENIX Association (2004)
Penix, J., Visser, W., Engstrom, E., Larson, A., Weininger, N.: Verification of time partitioning in the deos scheduler kernel. In: Proceedings of the 22nd international conference on Software engineering, pp. 488–497. ACM Press, New York (2000)
Robby, M.B.D., Hatcliff, J.: 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 (2003)
Robby, E.R., Dwyer, M., Hatcliff, J.: 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)
Tkachuk, O., Dwyer, M., Pasareanu, C.: Automated environment generation for software model checking. In: Proceedings of the 18th International Conference on Automated Software Engineering (October 2003)
Tkachuk, O., Dwyer, M.B.: Adapting side effects analysis for modular program model checking. In: Proceedings of the Fourth joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (September 2003)
Zhu, H., Hall, P., May, J.: Software unit test coverage and adequacy. ACM Computing Surveys 29(4), 366–427 (1997)
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
RodrÃguez, E., Dwyer, M.B., Hatcliff, J., Robby (2005). A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking. In: Barthe, G., Burdy, L., Huisman, M., Lanet, JL., Muntean, T. (eds) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. CASSIS 2004. Lecture Notes in Computer Science, vol 3362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30569-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-30569-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24287-1
Online ISBN: 978-3-540-30569-9
eBook Packages: Computer ScienceComputer Science (R0)