Time-Optimal Real-Time Test Case Generation Using Uppaal

  • Anders Hessel
  • Kim G. Larsen
  • Brian Nielsen
  • Paul Pettersson
  • Arne Skou
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2931)


Testing is the primary software validation technique used by industry today, but remains ad hoc, error prone, and very expensive. A promising improvement is to automatically generate test cases from formal models of the system under test.

We demonstrate how to automatically generate real-time conformance test cases from timed automata specifications. Specifically we demonstrate how to efficiently generate real-time test cases with optimal execution time i.e test cases that are the fastest possible to execute. Our technique allows time optimal test cases to be generated using manually formulated test purposes or generated automatically from various coverage criteria of the model.


Test Sequence Test Suite Test Purpose Coverage Criterion System Under Test 
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.
    Aho, A.V., Dahbura, A.T., Lee, D., Uyar, M.Ü.: An Optimization Technique for Protocol Conformance Test Generation Based on UIO Sequences and Rural Chinese Postman Tours. IEEE Transactions on Communications 39(11), 1604–1615 (1991)CrossRefGoogle Scholar
  2. 2.
    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
  3. 3.
    Bosscher, D., Polak, I., Vaandrager, F.: Verification of an Audio-Control Protocol. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863. Springer, Heidelberg (1994)Google Scholar
  4. 4.
    Bozga, M., Fernandez, J.-C., Ghirvu, L., Jard, C., Jéron, T., Kerbrat, A., Morel, P., Mounier, L.: Verification and Test Generation for the SSCOP Protocol. Science of Computer Programming 36(1), 27–52 (2000)CrossRefGoogle Scholar
  5. 5.
    Cardell-Oliver, R.: Conformance Testing of Real-Time Systems with Timed Automata. Formal Aspects of Computing 12(5), 350–371 (2000)zbMATHCrossRefGoogle Scholar
  6. 6.
    Castanet, R., Koné, O., Laurençot, P.: On The Fly Test Generation for Real- Time Protocols. In: International Conference in Computer Communications and Networks, Lafayette, Lousiana, USA, October 12-15. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  7. 7.
    Clarke, D., Lee, I.: Automatic Test Generation for the Analysis of a Real-Time System: Case Study. In: 3rd IEEE Real-Time Technology and Applications Symposium (1997)Google Scholar
  8. 8.
    En-Nouaary, A., Dssouli, R., Khendek, F., Elqortobi, A.: Timed Test Cases Generation Based on State Characterization Technique. In: 19th IEEE Real-Time Systems Symposium (RTSS 1998), December 2–4, pp. 220–229 (1998)Google Scholar
  9. 9.
    Higashino, T., Nakata, A., Taniguchi, K., Cavalli, A.R.: Generating Test Cases for a Timed I/O Automaton Model. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) Testing of Communicating Systems: Method and Applications, IFIP TC6 12th International Workshop on Testing Communicating Systems (IWTCS), Budapest, Hungary, September 1-3. IFIP Conference Proceedings, vol. 147, pp. 197–214. Kluwer, Dordrecht (1999)Google Scholar
  10. 10.
    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
  11. 11.
    Khoumsi, A.: A method for testing the conformance of real-time systems. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 331. 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.
    Lee, D., Yannakakis, M.: Principles and Methods of Testing Finite State Machines—A Survey. Proceedings of the IEEE 84(8), 1090–1123 (1996)CrossRefGoogle Scholar
  14. 14.
    Mandrioli, D., Morasca, S., Morzenti, A.: Generating Test Cases for Real-Time Systems from Logic Specifications. ACM Transactions on Computer Systems 13(4), 365–398 (1995)CrossRefGoogle Scholar
  15. 15.
    Nielsen, B., Skou, A.: Automated Test Generation from Timed Automata. International Journal on Software Tools for Technology Transfer (STTT), 4, Digital Object Identifier (DOI) 10.1007/s10009-002-0094-1 (2002) (to appear)Google Scholar
  16. 16.
    Peleska, J.: Hardware/Software Integration Testing for the new Airbus Aircraft Families. In: Wolis, A., Schieferdecker, I., König, H. (eds.) Testing of Communicating Systems XIV. Application to Internet Technologies and Services, pp. 335–351. Kluwer Academic Publishers, Dordrecht (2002)Google Scholar
  17. 17.
    Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing Timed Automata. Theoretical Computer Science 254(1-2), 225–257 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Tretmans, J., Belinfante, A.: Automatic testing with formal methods. In: EuroSTAR 1999: 7th European Int. Conference on Software Testing, Analysis & Review, Galway, Ireland, November 8–12. EuroStar Conferences (1999)Google Scholar
  19. 19.
    Uyar, M.Ü., Fecko, M.A., Sethi, A.S., Amar, P.D.: Testing Protocols Modeled as FSMs with Timing Parameters. Computer Networks: The International Journal of Computer and Telecommunication Networking 31(18), 1967–1998 (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Anders Hessel
    • 1
  • Kim G. Larsen
    • 2
  • Brian Nielsen
    • 2
  • Paul Pettersson
    • 1
  • Arne Skou
    • 2
  1. 1.Department of Information TechnologyUppsala UniversityUppsalaSweden
  2. 2.Department of Computer ScienceAalborg UniversityAalborgDenmark

Personalised recommendations