Testing Real-Time Systems under Uncertainty

  • Alexandre David
  • Kim Guldstrand Larsen
  • Shuhao Li
  • Marius Mikucionis
  • Brian Nielsen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)


Model-based testing is a promising technique for improving the quality of testing by automatically generating an efficient set of provably valid test cases from a system model. Testing embedded real-time systems is challenging because it must deal with timing, concurrency, processing and computation of complex mixed discrete and continuous signals, and limited observation and control. Whilst several techniques and tools have been proposed, few deals systematically with models capturing the indeterminacy resulting from concurrency, timing and limited observability and controllability. This paper proposes a number of model-based test generation principles and techniques that aim at efficient testing of timed systems under uncertainty.


Test Purpose Winning Strategy Test Case Generation Partial Observability Conformance Testing 
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.
    Alur, R., Courcoubetis, C., Yannakakis, M.: Distinguishing tests for nondeterministic and probabilistic machines. In: Proc. STOC 1995, pp. 363–372. ACM Press, New York (1995)Google Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bertrand, N., Jéron, T., Stainer, A., Krichen, M.: Off-line test selection with test purposes for non-deterministic timed automata. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 96–111. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  4. 4.
    Blass, A., Gurevich, Y., Nachmanson, L., Veanes, M.: Play to test. In: Grieskamp, W., Weise, C. (eds.) FATES 2005. LNCS, vol. 3997, pp. 32–46. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Bohnenkamp, H., Stoelinga, M.: Quantitative testing. In: Proc. EMSOFT 2008. ACM, New York (2008)Google Scholar
  6. 6.
    Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed control with partial observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 180–192. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Briones, L.B., Brinksma, E.: A test generation framework for quiescent real-time systems. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 64–78. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 192–206. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. 10.
    David, A., Larsen, K.G., Li, S., Nielsen, B.: Cooperative testing of timed systems. In: Proc. MBT 2008 (2008)Google Scholar
  11. 11.
    David, A., Larsen, K.G., Li, S., Nielsen, B.: A game-theoretic approach to real-time system testing. In: Proc. DATE 2008 (2008)Google Scholar
  12. 12.
    David, A., Larsen, K.G., Li, S., Nielsen, B.: Timed testing under partial observability. In: Proc. 2nd International Conference on Software Testing, Verification and Validation (ICST 2009), Denver, Colorado, USA, pp. 61–70. IEEE Computer Society, Los Alamitos (2009)CrossRefGoogle Scholar
  13. 13.
    Daws, C., Olivero, A., Yovine, S.: Verifying ET-LOTOS programs with Kronos. In: Hogrefe, D., Leue, S. (eds.) Proc. of 7th Int. Conf. on Formal Description Techniques. North-Holland, Amsterdam (1994)Google Scholar
  14. 14.
    Dill, D.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  15. 15.
    En-Nouaary, A., Dssouli, R., Khendek, F., Elqortobi, A.: Timed test cases generation based on state characterization technique. In: Proc. RTSS 1998, pp. 220–229 (1998)Google Scholar
  16. 16.
    Hessel, A., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A., Larsen, K.G.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Khoumsi, A., Jéron, T., Marchand, H.: Test cases generation for nondeterministic real-time systems. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 131–146. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Krichen, M., Tripakis, S.: Black-box conformance testing for real-time systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Formal Methods in System Design 34(3), 238–304 (2009)CrossRefzbMATHGoogle Scholar
  20. 20.
    Larsen, K.G., Mikucionis, M., Nielsen, B.: Online testing of real-time systems using uppaal. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 79–94. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  21. 21.
    Larsen, K.G., Mikucionis, M., Nielsen, B., Skou, A.: Testing real-time embedded software using uppaal-tron: an industrial case study. In: Wolf, W. (ed.) EMSOFT, pp. 299–306. ACM, New York (2005)Google Scholar
  22. 22.
    Li, S.: Games and Scenarios for Real-Time System Validation. PhD thesis, Dept. of Computer Science, Aalborg University (2010)Google Scholar
  23. 23.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  24. 24.
    Nielsen, B., Skou, A.: Automated test generation from timed automata. STTT 5(1), 59–77 (2003)CrossRefzbMATHGoogle Scholar
  25. 25.
    Rokicki, T.G., Myers, C.J.: Automatic verification of timed circuits. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 468–480. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  26. 26.
    Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing timed automata. TCS 254(1-2), 225–257 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Tretmans, J.: Testing concurrent systems: A formal approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 46–65. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  28. 28.
    Tretmans, J., Schmaltz, J.: On conformance testing for timed systems. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 250–264. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  29. 29.
    Vain, J., Raiend, K., Kull, A., Ernits, J.P.: Synthesis of test purpose directed reactive planning tester for nondeterministic systems. In: Kurt Stirewalt, R.E., Egyed, A., Fischer, B. (eds.) ASE, pp. 363–372. ACM, New York (2007)CrossRefGoogle Scholar
  30. 30.
    de Vries, R.G., Tretmans, J.: On-the-fly conformance testing using Spin. Software Tools for Technology Transfer 2(4), 382–393 (2000)CrossRefzbMATHGoogle Scholar
  31. 31.
    Yannakakis, M.: Testing, optimizaton, and games. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 28–45. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Alexandre David
    • 1
  • Kim Guldstrand Larsen
    • 1
  • Shuhao Li
    • 1
  • Marius Mikucionis
    • 1
  • Brian Nielsen
    • 1
  1. 1.Center for Embedded Software Systems (CISS)Aalborg UniversityAalborgDenmark

Personalised recommendations