Auto-generating Test Sequences Using Model Checkers: A Case Study

  • Mats P. E. Heimdahl
  • Sanjai Rayadurgam
  • Willem Visser
  • George Devaraj
  • Jimin Gao
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2931)


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.


Model Checker Test Suite Coverage Criterion Symbolic Model Check Decision Coverage 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Callahan, J., Schneider, F., Easterbrook, S.: Specification-based testing using model checking. In: Proceedings of the SPIN Workshop (August 1996)Google Scholar
  4. 4.
    Chilenski, J.J., Miller, S.P.: Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, 193–200 (September 1994)Google Scholar
  5. 5.
    Choi, Y., Heimdahl, M.: Model checking RSML− erequirements. In: Proceedings of the 7th IEEE/IEICE International Symposium on High Assurance Systems Engineering (October 2002)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. Software Engineering Notes 24(6), 146–162 (1999)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Henzinger, T.A., Jhala, R., Majumdar, R., Majumdar, R.: Lazy abstraction. In: Proceedings of the 29th Symposium on Principles of Programming Languages (January 2002)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    NuSMV: A New Symbolic Model Checking, Available at
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    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)Google Scholar
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    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)Google Scholar
  25. 25.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Mats P. E. Heimdahl
    • 1
  • Sanjai Rayadurgam
    • 1
  • Willem Visser
    • 2
  • George Devaraj
    • 1
  • Jimin Gao
    • 1
  1. 1.Department of Computer Science and EngineeringUniversity of MinnesotaMinneapolisUSA
  2. 2.NASA Ames Research CenterMoffett Field

Personalised recommendations