Connectivity Testing Through Model-Checking

  • Jens Chr. Godskesen
  • Brian Nielsen
  • Arne Skou
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3235)


In this paper we show how to automatically generate test sequences that are aimed at testing the interconnections of embedded and communicating systems. Our proposal is based on the connectivity fault model proposed by [8], where faults may occur in the interface between the software and its environment rather than in the software implementation.

We show that the test generation task can be carried out by solving a reachability problem in a system consisting essentially of a specification of the communicating system and its fault model. Our technique can be applied using most off-the-shelf model-checking tools to synthesize minimal test sequences, and we demonstrate it using the UppAal real-time model-checker.

We present two algorithms for generating minimal tests: one for single faults and one for multiple faults. Moreover, we demonstrate how to exploit the unique time- and cost-planning- facilities of UppAal to derive cheapest possible test suites for restricted types of timed systems.


Test Suite Label Transition System System Under Test Speed Controller Connectivity Error 
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.


  1. 1.
    Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Ammann, P., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: ICFEM, p. 46 (1998)Google Scholar
  3. 3.
    Ammann, P., Ding, W., Xu, D.: Using a model checker to test safety propertiesGoogle Scholar
  4. 4.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient Guiding Towards Cost-Optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Callahan, J., Schneider, F., Easterbrook, S.: Automated software testing using modelchecking. In: 1996 SPIN Workshop (August 1996); Also WVU Report NASAIVV-96-022Google Scholar
  6. 6.
    Engels, A., Feijs, L., Mauw, S.: Test generation for intelligent networks using model checking. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, Springer, Heidelberg (1997)CrossRefGoogle Scholar
  7. 7.
    Gargantini, A., Heitmeyer, C.L.: Using model checking to generate tests from requirements specifications. In: ESEC / SIGSOFT FSE, pp. 146–162 (1999)Google Scholar
  8. 8.
    Godskesen, J.C.: Complexity issues in connectivity testing. In: Brinksma, E., Tretmans, J. (eds.) Proceedings of the Workshop on Formal Approaches to Testing of Software, FATES 2001, Aalborg, Denmark, August 25 (2001)Google Scholar
  9. 9.
    Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-Optimal Test Cases for Real-Time Systems. In: 3rd Intl. Workshop on Formal Approaches to Testing of Software (FATES 2003), Montréal, Québec, Canada (October 2003)Google Scholar
  10. 10.
    Hong, H., Lee, I., Sokolsky, O., Cha, S.: Automatic test generation from statecharts using model checking. In: Brinksma, E., Tretmans, J. (eds.) Workshop on Formal Approaches to Testing of Software, FATES 2001, Aalborg, Denmark, August 25 (2001)Google Scholar
  11. 11.
    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, pp. 327–341. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: Efficient cost-optimal reachability for priced timed automat. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    Larsen, K.G., Pettersson, P., Yi, W.: UppAal in a Nutshell. International Journal on Software Tools for Technology Transfer 1(1), 134–152 (1997)CrossRefzbMATHGoogle Scholar
  14. 14.
    Magee, Kramer: Concurrency: State Models and Java Programs. Wiley, Chichester (2002)zbMATHGoogle Scholar
  15. 15.
    Heimdahl, M.P.E., Rayadurgam, S., Visser, W., Devaraj, G., Gao, J.: Auto-generating Test Sequences Using Model Checkers: A Case Study. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 42–59. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Springintveld, J.G., Vaandrager, F.W., D’Argenio, P.R.: Testing timed automata. Theoretical Computer Science 254(1-2) (March 2001)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • Jens Chr. Godskesen
    • 1
    • 2
  • Brian Nielsen
    • 1
  • Arne Skou
    • 1
  1. 1.Center of Embedded Software SystemsAalborg UniversityAalborgDenmark
  2. 2.IT-University of CopenhagenCopenhagen NV.Denmark

Personalised recommendations