Skip to main content
SpringerLink
Log in

Compositional Testing of Real-Time Systems

  • Chapter
  • First Online:
Book cover ModelEd, TestEd, TrustEd

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10500))

Abstract

In this paper we revisit the notion of compositional testing in the setting of real-time systems. In particular, we introduce crucial notions of real-time conformance testing and compositional verification of real-time systems. We illustrate these notions on a Small University example, and show how the tools Uppaal Tron, Uppaal Ecdar and Uppaal SMC provide strong support for an efficient compositional testing methodology.

Three methods for managing a small university.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Invited tutorial at ETAPS 2017.

  2. 2.

    In contrast to general timed automata, complementation is possible due to the assumption that TIOA’s are deterministic.

References

  1. Aiguier, M., Boulanger, F., Kanso, B.: A formal abstract framework for modelling and testing complex software systems. Theoret. Comput. Sci. 455, 66–97 (2012). International Colloquium on Theoretical Aspects of Computing (2010)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Kanso, B., Chebaro, O.: Compositional testing for FSM-based models. Int. J. Softw. Eng. Appl. (IJSEA) 5(3) (2014)

    Google Scholar 

  4. Boudjadar, A., David, A., Kim, J.H., Larsen, K.G., Mikucionis, M., Nyman, U., Skou, A.: Degree of schedulability of mixed-criticality real-time systems with probabilistic sporadic tasks. In: 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, 1–3 September 2014, pp. 126–130. IEEE Computer Society (2014)

    Google Scholar 

  5. Briones, L.B.: Assume-guarantee reasoning with ioco testing relation. In: Proceedings of the 22nd IFIP International Conference on Testing Software and Systems (2010)

    Google Scholar 

  6. Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 260–275. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_25

    Chapter  Google Scholar 

  7. Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Li, G., Bøgsted Poulsen, D., Stainer, A.: Monitor-based statistical model checking for weighted metric temporal logic. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 168–182. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28717-6_15

    Chapter  Google Scholar 

  8. Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Mikučionis, M., Bøgsted Poulsen, D.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 449–463. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28891-3_39

    Chapter  Google Scholar 

  9. Daca, P., Henzinger, T.A., Krenn, W., Nickovic, D.: Compositional specifications for ioco testing. In: Seventh IEEE International Conference on Software Testing, Verification and Validation, ICST, 31 March 2014–4 April 2014, Cleveland, Ohio, USA, pp. 373–382. IEEE Computer Society (2014)

    Google Scholar 

  10. David, A., Du, D., Larsen, K.G., Mikucionis, M., Skou, A.: An evaluation framework for energy aware buildings using statistical model checking. Sci. China Inf. Sci. 55(12), 2694–2707 (2012)

    Article  Google Scholar 

  11. David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of herschel-planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 293–307. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34032-1_28

    Chapter  Google Scholar 

  12. David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397–415 (2015)

    Article  Google Scholar 

  13. David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. STTT 17(3), 351–367 (2015)

    Article  Google Scholar 

  14. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_7

    Chapter  Google Scholar 

  15. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_27

    Chapter  Google Scholar 

  16. David, A., Larsen, K.G., Legay, A., Nyman, U., Traonouez, L., Wasowski, A.: Real-time specifications. STTT 17(1), 17–45 (2015)

    Article  Google Scholar 

  17. David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 365–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15643-4_29

    Chapter  Google Scholar 

  18. David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Johansson and Yi [21], pp. 91–100

    Google Scholar 

  19. David, N., David, A., Hansen, R.R., Larsen, K.G., Legay, A., Olesen, M.C., Probst, C.W.: Modelling social-technical attacks with timed automata. In: Bertino, E., You, I. (eds.) Proceedings of the 7th ACM CCS International Workshop on Managing Insider Security Threats, MIST 2015, Denver, Colorado, USA, 16 October 2015, pp. 21–28. ACM (2015)

    Google Scholar 

  20. Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78917-8_3

    Chapter  Google Scholar 

  21. Johansson, K.H., Yi, W. (eds.): Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, 12–15 April 2010. ACM (2010)

    Google Scholar 

  22. Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Form. Methods Syst. Des. 34(3), 238–304 (2009)

    Article  MATH  Google Scholar 

  23. Larsen, K.G., Mikucionis, M., Nielsen, B., Skou, A.: Testing real-time embedded software using uppaal-tron: an industrial case study. In: Proceedings of the 5th ACM International Conference on Embedded Software, EMSOFT 2005, pp. 299–306. ACM, New York (2005)

    Google Scholar 

  24. 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). doi:10.1007/978-3-540-31848-4_6

    Chapter  Google Scholar 

  25. Mikučionis, M., Larsen, K.G., Nielsen, B.: T-uppaal: online model-based testing of real-time systems. In: Proceedings of the 19th IEEE International Conference on Automated Software Engineering, ASE 2004, pp. 396–397. IEEE Computer Society, Washington, DC, USA (2004)

    Google Scholar 

  26. Tretmans, J.: A formal approach to conformance testing. In: Rafiq, O. (ed.) Protocol Test Systems, VI, Proceedings of the IFIP TC6/WG6.1 Sixth International Workshop on Protocol Test Systems, Pau, France, 28–30 September 1993. IFIP Transactions, vol. C-19, pp. 257–276. North-Holland (1993)

    Google Scholar 

  27. van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 86–100. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24617-6_7

    Chapter  Google Scholar 

  28. van Glabbeek, R.J., Höfner, P., Portmann, M., Tan, W.L.: Modelling and verifying the AODV routing protocol. Distrib. Comput. 29(4), 279–315 (2016)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Kim G. Larsen, Marius Mikučionis, Brian Nielsen & Ulrik Nyman

  2. INRIA, Rennes, France

    Axel Legay

Authors
  1. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marius Mikučionis
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Brian Nielsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ulrik Nyman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kim G. Larsen .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  2. University of Twente, Enschede, The Netherlands

    Rom Langerak

  3. University of Twente, Enschede, The Netherlands

    Arend Rensink

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Larsen, K.G., Legay, A., Mikučionis, M., Nielsen, B., Nyman, U. (2017). Compositional Testing of Real-Time Systems. In: Katoen, JP., Langerak, R., Rensink, A. (eds) ModelEd, TestEd, TrustEd. Lecture Notes in Computer Science(), vol 10500. Springer, Cham. https://doi.org/10.1007/978-3-319-68270-9_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68270-9_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68269-3

  • Online ISBN: 978-3-319-68270-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation