Abstract
Use of model-checking approaches for test generation from requirement models have been proposed by several researchers. These approaches leverage the witness (or counter-example) generation capability of model-checkers for constructing test cases. Test criteria are expressed as temporal properties. Witness traces generated for these properties are instantiated to create complete test sequences, satisfying the criteria. State-space explosion can, however, adversely impact model-checking and hence such test generation. Thus, there is a need to validate these approaches against realistic industrial sized system models to learn how well these approaches scale. To this end, we conducted a case study using six models of progressively increasing complexity of the mode-logic in a flight-guidance system, written in the RSML− e language. We developed a framework for specification-based test generation using the NuSMV model-checker and code based test case generation using Java Pathfinder, and collected time and resource usage data for generating test cases using symbolic, bounded, and explicit state model-checking algorithms. This paper briefly discusses the approach, presents the results from the study and analyzes its implications.
This work has been partially supported by NASA grant NAG-1-224 and NASA contract NCC-01-001. We also want to thank the McKnight Foundation for their generous support over the years.
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
Ammann, P.E., Black, P.E.: A specification-based coverage metric to evaluate test sets. In: Proceedings of the Fourth IEEE International Symposium on High-Assurance Systems Engineering, November 1999. IEEE Computer Society, Los Alamitos (1999)
Ammann, P.E., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: Proceedings of the Second IEEE International Conference on Formal Engineering Methods (ICFEM 1998), November 1998, pp. 46–54. IEEE Computer Society, Los Alamitos (1998)
Callahan, J., Schneider, F., Easterbrook, S.: Specification-based testing using model checking. In: Proceedings of the SPIN Workshop (August 1996)
Chilenski, J.J., Miller, S.P.: Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, 193–200 (September 1994)
Choi, Y., Heimdahl, M.: Model checking RSML− erequirements. In: Proceedings of the 7th IEEE/IEICE International Symposium on High Assurance Systems Engineering (October 2002)
Choi, Y., Rayadurgam, S., Heimdahl, M.: Automatic abstraction for model checking software systems with interrelated numeric constraints. In: Proceedings of the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE-9), September 2001, pp. 164–174 (2001)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counter example-guided abstraction refinement. In: Proceedings of the 12th International Conference on Computer Aided Verification, July 2000, pp. 154–169 (2000)
Engels, A., Feijs, L.M.G., Mauw, S.: Test generation for intelligent networks using model checking. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 384–398. Springer, Heidelberg (1997)
Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. Software Engineering Notes 24(6), 146–162 (1999)
Groce, A., Visser, W.: Model checking java programs using structural heuristics. In: Proceedings of the International Symposium on Software Testign and Analysis 2002, Rome, Italy (July 2002)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
Heimdahl, M.P.E., Rayadurgam, S., Visser, W.: Specification centered testing. In: Proceedings of The First International Workshop on Automated Program Analysis, Testing and Verificaiton, ICSE 2000 (2000)
Henzinger, T.A., Jhala, R., Majumdar, R., Majumdar, R.: Lazy abstraction. In: Proceedings of the 29th Symposium on Principles of Programming Languages (January 2002)
Hong, H.S., Cha, S.D., Lee, I., Sokolsky, O., Ural, H.: Data flow testing as model checking. In: Proceedings of 2003 International Confernece on Software Engineering, Portland, Oregon (May 2003)
Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 327. Springer, Heidelberg (2002)
Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Warsaw, Poland (April 2003)
Leveson, N.G., Heimdahl, M.P.E., Hildreth, H., Reese, J.D.: Requirements Specification for Process-Control Systems. IEEE Transactions on Software Engineering 20(9), 684–706 (1994)
NuSMV: A New Symbolic Model Checking, Available at http://nusmv.irst.itc.it/
Rayadurgam, S., Heimdahl, M.P.E.: Coverage based test-case generation using model checkers. In: Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001), April 2001, pp. 83–91. IEEE Computer Society, Los Alamitos (2001)
Rayadurgam, S., Heimdahl, M.P.E.: Test-Sequence Generation from Formal Requirement Models. In: Proceedings of the 6th IEEE International Symposium on the High Assurance Systems Engineering (HASE 2001), Boca Raton, Florida (October 2001)
Thompson, J.M., Heimdahl, M.P.E., Miller, S.P.: Specification based prototyping for embedded systems. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol. 1687, pp. 163–179. Springer, Heidelberg (1999)
Thompson, J.M., Whalen, M.W., Heimdahl, M.P.E.: Requirements capture and evaluation in Nimbus: The light-control case study. Journal of Universal Computer Science 6(7), 731–757 (2000)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Symposium on Logic in Computer Science, Cambridge, June 1986, pp. 322–331 (1986)
Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proceedings of the 15th International Conference on Automated Software Engineering, Grenoble, France (September 2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heimdahl, M.P.E., Rayadurgam, S., Visser, W., Devaraj, G., Gao, J. (2004). Auto-generating Test Sequences Using Model Checkers: A Case Study. In: Petrenko, A., Ulrich, A. (eds) Formal Approaches to Software Testing. FATES 2003. Lecture Notes in Computer Science, vol 2931. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24617-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-24617-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20894-5
Online ISBN: 978-3-540-24617-6
eBook Packages: Springer Book Archive