Advertisement

20 Years of Real Real Time Model Validation

  • Kim Guldstrand Larsen
  • Florian Lorber
  • Brian Nielsen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

In this paper we review 20 years of significant industrial application of the Uppaal Tool Suite for model-based validation, performance evaluation and synthesis. The paper will highlight a number of selected cases, and discuss successes and pitfalls in achieving industrial impact as well as tool sustainability in an academic setting.

References

  1. 1.
    Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 1997), 3–5 December 1997. IEEE Computer Society, San Francisco (1997)Google Scholar
  2. 2.
    Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11–14 September 2006. IEEE Computer Society, Riverside (2006)Google Scholar
  3. 3.
    Mikucionis, M., Larsen, K.G., Nielsen, B.: T-uppaal: online model-based testing of real-time systems. In: Grunbacher, P. (ed.) 19th IEEE International Conference on Automated Software Engineering (ASE 2004) Proceedings, pp. 396–397, United States, IEEE Computer Society Press (2004). ISSN; 1068–3062Google Scholar
  4. 4.
    Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Benedetto and Sangiovanni-Vincentelli [10], pp. 49–62CrossRefGoogle Scholar
  5. 5.
    Asaadi, H.R., Khosravi, R., Mousavi, M.R., Noroozi, N.: Towards model-based testing of electronic funds transfer systems. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 253–267. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-29320-7_17CrossRefGoogle Scholar
  6. 6.
    Behrmann, G., et al.: UPPAAL-tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73368-3_14CrossRefGoogle Scholar
  7. 7.
    Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006) [2], 11–14 September 2006, Riverside, California, USA, pp. 125–126Google Scholar
  8. 8.
    Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exper. 41(2), 133–142 (2011)CrossRefGoogle Scholar
  9. 9.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Benedetto and Sangiovanni-Vincentelli [10], pp. 147–161CrossRefGoogle Scholar
  10. 10.
    Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.): HSCC 2001. LNCS, vol. 2034. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45351-2CrossRefGoogle Scholar
  11. 11.
    Bengtsson, J., et al.: Verification of an audio protocol with bus collision using Uppaal. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 244–256. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-61474-5_73CrossRefGoogle Scholar
  12. 12.
    Bisgaard, M., et al.: Battery-aware scheduling in low orbit: the GomX–3 case. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 559–576. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-48989-6_34CrossRefGoogle Scholar
  13. 13.
    Bosscher, D., Polak, I., Vaandrager, F.: Verification of an audio control protocol. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 170–192. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58468-4_165CrossRefGoogle Scholar
  14. 14.
    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
  15. 15.
    Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.): TACAS 1995. LNCS, vol. 1019. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60630-0CrossRefGoogle Scholar
  16. 16.
    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).  https://doi.org/10.1007/11539452_9CrossRefGoogle Scholar
  17. 17.
    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).  https://doi.org/10.1007/978-3-540-75596-8_15CrossRefMATHGoogle Scholar
  18. 18.
    D’Argenio, P.R., Katoen, J.-P., Ruys, T.C., Tretmans, J.: The bounded retransmission protocol must be on time!. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0035403CrossRefGoogle Scholar
  19. 19.
    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)CrossRefGoogle Scholar
  20. 20.
    David, A., et al.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129–145. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_10CrossRefGoogle Scholar
  21. 21.
    David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206–211. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_16CrossRefGoogle Scholar
  22. 22.
    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).  https://doi.org/10.1007/978-3-642-34032-1_28CrossRefGoogle Scholar
  23. 23.
    David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Schedulability of herschel revisited using statistical model checking. STTT 17(2), 187–199 (2015)CrossRefGoogle Scholar
  24. 24.
    David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397–415 (2015)CrossRefGoogle Scholar
  25. 25.
    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)CrossRefGoogle Scholar
  26. 26.
    David, A., et al.: 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).  https://doi.org/10.1007/978-3-642-24310-3_7CrossRefGoogle Scholar
  27. 27.
    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).  https://doi.org/10.1007/978-3-642-22110-1_27CrossRefGoogle Scholar
  28. 28.
    David, A., Larsen, K.G., Legay, A., Nyman, U., Traonouez, L., Wasowski, A.: Real-time specifications. STTT 17(1), 17–45 (2015)CrossRefGoogle Scholar
  29. 29.
    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).  https://doi.org/10.1007/978-3-642-15643-4_29CrossRefGoogle Scholar
  30. 30.
    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, 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, pp. 91–100. ACM (2010)Google Scholar
  31. 31.
    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
  32. 32.
    de Vries, R.G., Tretmans, J.: On-the-fly conformance testing using SPIN. STTT 2(4), 382–393 (2000)CrossRefGoogle Scholar
  33. 33.
    Eriksen, A.B., Huang, C., Kildebogaard, J., Lahrmann, H., Larsen, K.G., Muniz, M., Taankvist, J.H.: Uppaal stratego for intelligent traffic lights. In: ITS European Congress (2017)Google Scholar
  34. 34.
    Gerke, M., Ehlers, R., Finkbeiner, B., Peter, H.-J.: Model checking the flexray physical layer protocol. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 132–147. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15898-8_9CrossRefGoogle Scholar
  35. 35.
    Havelund, K., Larsen, K.G., Skou, A.: Formal verification of a power controller using the real-time model checker Uppaal. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 277–298. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48778-6_17CrossRefGoogle Scholar
  36. 36.
    Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL. In: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 1997) [1], 3–5 December 1997, San Francisco, CA, USA, pp. 2–13 (1997)Google Scholar
  37. 37.
    Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal test cases for real-time systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 234–245. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-40903-8_19CrossRefGoogle Scholar
  38. 38.
    Kim, J.H., Larsen, K.G., Nielsen, B., Mikučionis, M., Olsen, P.: Formal analysis and testing of real-time automotive systems using UPPAAL tools. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 47–61. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-19458-5_4CrossRefGoogle Scholar
  39. 39.
    Larsen, K., et al.: As cheap as possible: effcient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44585-4_47CrossRefGoogle Scholar
  40. 40.
    Larsen, K.G., Mikučionis, M., Muñiz, M., Srba, J., Taankvist, J.H.: Online and compositional learning of controllers with application to floor heating. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 244–259. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_14CrossRefGoogle Scholar
  41. 41.
    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).  https://doi.org/10.1007/978-3-540-31848-4_6CrossRefMATHGoogle Scholar
  42. 42.
    Larsen, K.G., Mikucionis, M., Nielsen, B., Skou, A.: Testing real-time embedded software using UPPAAL-TRON: an industrial case study. In: Wolf, W.H. (ed.) EMSOFT 2005, 18–22 September 2005, 5th ACM International Conference on Embedded Software, Proceedings, Jersey City, NJ, USA, pp. 299–306. ACM (2005)Google Scholar
  43. 43.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1–2), 134–152 (1997)CrossRefGoogle Scholar
  44. 44.
    Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gear controller. STTT 3(3), 353–368 (2001)MATHGoogle Scholar
  45. 45.
    Mikucionis, M., Larsen, K.G., Nielsen, B.: T-UPPAAL: online model-based testing of real-time systems. In: 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20–25 September 2004, Linz, Austria, pp. 396–397. IEEE Computer Society (2004)Google Scholar
  46. 46.
    Mikučionis, M., et al.: Schedulability analysis using uppaal: Herschel-Planck case study. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 175–190. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16561-0_21CrossRefGoogle Scholar
  47. 47.
    Nielsen, B.: Specification and Test of Real-Time Systems. Ph.D thesis. Aalborg University (2000)Google Scholar
  48. 48.
    Nielsen, B., Skou, A.: Automated test generation from timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 343–357. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45319-9_24CrossRefGoogle Scholar
  49. 49.
    Nielsen, B., Skou, A.: Test generation for time critical systems: tool and case study. In: 13th Euromicro Conference on Real-Time Systems, Delft, The Netherlands, pp. 155–162, June 2001Google Scholar
  50. 50.
    Romijn, J.: A timed verification of the IEEE 1394 leader election protocol. Formal Methods Syst. Des. 19(2), 165–194 (2001)CrossRefGoogle Scholar
  51. 51.
    Rütz, C.: Timed model-based conformance testing - a case study using tron: testing key states of automated trust anchor updating (rfc 5011) in autotrust. B.Sc. thesis (2010)Google Scholar
  52. 52.
    Tretmans, J.: A formal approach to conformance testing C-19, 257–276 (1993)Google Scholar
  53. 53.
    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)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Kim Guldstrand Larsen
    • 1
  • Florian Lorber
    • 1
  • Brian Nielsen
    • 1
  1. 1.Department of Computer ScienceAalborg UniversityAalborgDenmark

Personalised recommendations