Model-Based Testing for Avionic Systems Proven Benefits and Further Challenges

  • Jan PeleskaEmail author
  • Jörg Brauer
  • Wen-ling Huang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11247)


In this article, we report on the transition of model-based testing (MBT) from a widely discussed research discipline to an accepted technology that is currently becoming state of the art in industry; in particular, in the field of safety-critical systems testing. It is reviewed how focal points of MBT-related research in the past have found their way into today’s commercial MBT products. We describe the benefits of MBT that are – from our experience – most appreciated by practitioners. Moreover, some interesting open challenges are described, and potential future solutions are presented. The material presented in this paper is based on our practical experience with recent MBT campaigns performed for Airbus in Germany.


Model-based testing Avionic systems HW/SW integration testing Scenario-based testing 


  1. 1.
    Araujo, H.L.S., Carvalho, G., Mohaqeqi, M., Mousavi, M.R., Sampaio, A.: Sound conformance testing for cyber-physical systems: theory and implementation. Sci. Comput. Program. 162, 35–54 (2018). Scholar
  2. 2.
    Banci, M., Fantechi, A., Gnesi, S., Lombardi, G.: Model driven development and code generation: an automotive case study. In: Gaudin, E., Najm, E., Reed, R. (eds.) SDL 2007. LNCS, vol. 4745, pp. 19–34. Springer, Heidelberg (2007). Scholar
  3. 3.
    Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5) (2006). arXiv:cs/0611029
  4. 4.
    Du Bousquet, L., Ramangalahy, S., Simon, S., Viho, C., Belinfante, A., de Vries, R.G.: Formal test automation: the conference protocol with TGV/TorX. In: Ural, H., Probert, R.L., v. Bochmann, G. (eds.) Testing of Communicating Systems. IAICT, vol. 48, pp. 221–228. Springer, Boston, MA (2000). Scholar
  5. 5.
    Brauer, J., Peleska, J., Schulze, U.: Efficient and trustworthy tool qualification for model-based testing tools. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 8–23. Springer, Heidelberg (2012). Scholar
  6. 6.
    Brauer, J., Schulze, U.: Model-based testing for avionics systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 657–661. Springer, Cham (2018). Scholar
  7. 7.
    Cavarra, A.: Data flow analysis and testing of abstract state machines. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 85–97. Springer, Heidelberg (2008). Scholar
  8. 8.
    Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. SE–4(3), 178–186 (1978)CrossRefGoogle Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  10. 10.
    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). Scholar
  11. 11.
    Hou, Z., Sanán, D., Tiu, A., Liu, Y.: A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. Archive of Formal Proofs 2016 (2016).
  12. 12.
    Huang, W., Peleska, J.: Complete model-based equivalence class testing. Softw. Tools Technol. Transfer 18(3), 265–283 (2016). Scholar
  13. 13.
    Huang, W., Peleska, J.: Complete model-based equivalence class testing for nondeterministic systems. Formal Aspects of Comput. 29(2), 335–364 (2017). Scholar
  14. 14.
    Huang, W., Peleska, J.: Model-based testing strategies and their (in)dependence on syntactic model representations. Int. J. Softw. Tools Technol. Transf. 20, 441–465 (2017). Scholar
  15. 15.
    Hübner, F., Huang, W., Peleska, J.: Experimental evaluation of a novel equivalence class partition testing strategy. Softw. Syst. Model. (2017).
  16. 16.
    Jensen, H.E., Larsen, K.G., Skou, A.: Modelling and analysis of a collision avoidance protocol using spin and UPPAAL. In: Grégoire, J., Holzmann, G.J., Peled, D.A. (eds.) The Spin Verification System, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, August 1996. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 33–50. DIMACS/AMS (1996).
  17. 17.
    Kästner, D., et al.: Timing validation of automotive software. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 93–107. Springer, Heidelberg (2008). Scholar
  18. 18.
    Kuhn, D.R., Kacker, R.N., Lei, Y.: Introduction to Combinatorial Testing. CRC Press, Boca Raton (2013)zbMATHGoogle Scholar
  19. 19.
    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).
  20. 20.
    Lee, J., Kang, S., Lee, D.: A survey on software product line testing. In: Proceedings of the 16th International Software Product Line Conference, SPLC 2012, vol. 1, pp. 31–40. ACM, New York (2012).
  21. 21.
    Mohacsi, S., Felderer, M., Beer, A.: A case study on the efficiency of model-based testing at the European space agency. In: 8th IEEE International Conference on Software Testing, Verification and Validation, ICST 2015, Graz, Austria, 13–17 April 2015, pp. 1–2. IEEE Computer Society (2015).
  22. 22.
    Mohacsi, S., Felderer, M., Beer, A.: Estimating the cost and benefit of model-based testing: a decision support procedure for the application of model-based testing in industry. In: 41st Euromicro Conference on Software Engineering and Advanced Applications, EUROMICRO-SEAA 2015, Madeira, Portugal, 26–28 August 2015, pp. 382–389. IEEE Computer Society (2015).
  23. 23.
    Neto, A.C.D., Travassos, G.H.: A picture from the model-based testing area: concepts, techniques, and challenges. Adv. Comput. 80, 45–120 (2010). Scholar
  24. 24.
    Object Management Group: OMG Systems Modeling Language (OMG SysML), Version 1.4. Technical report, Object Management Group (2015).
  25. 25.
    Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings Eighth Workshop on Model-Based Testing, Rome, Italy, 17th March 2013. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3–28. Open Publishing Association (2013)Google Scholar
  26. 26.
    Peleska, J.: Model-based avionic systems testing for the airbus family. In: 23rd IEEE European Test Symposium, ETS 2018, Bremen, Germany, 28 May–1 June 2018, pp. 1–10. IEEE (2018).
  27. 27.
    Peleska, J., Huang, W., Hübner, F.: A novel approach to HW/SW integration testing of route-based interlocking system controllers. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 32–49. Springer, Cham (2016). Scholar
  28. 28.
    Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 298–312. Springer, Heidelberg (2011). Scholar
  29. 29.
    Petrenko, A.: Checking experiments for symbolic input/output finite state machines. In: Ninth IEEE International Conference on Software Testing, Verification and Validation Workshops, ICST Workshops 2016, Chicago, IL, USA, 11–15 April 2016, pp. 229–237. IEEE Computer Society (2016).
  30. 30.
    Petrenko, A., Simao, A., Maldonado, J.C.: Model-based testing of software and systems: recent advances and challenges. Int. J. Softw. Tools Technol. Transf. 14(4), 383–386 (2012). Scholar
  31. 31.
    RTCA SC-205/EUROCAE WG-71: Software Considerations in Airborne Systems and Equipment Certification. Technical report, RTCA/DO-178C, RTCA Inc, 1140 Connecticut Avenue, N.W., Suite 1020, Washington, D.C. 20036, December 2011Google Scholar
  32. 32.
    Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495–511 (1994)CrossRefGoogle Scholar
  33. 33.
    Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. 22(5), 297–312 (2012). Scholar
  34. 34.
    Vasilevskii, M.P.: Failure diagnosis of automata. Kibernetika (Transl.) 4, 98–108 (1973)MathSciNetGoogle Scholar
  35. 35.
    Weißleder, S.: Test models and coverage criteria for automatic model-based test generation with UML state machines. Ph.D. thesis, Humboldt University of Berlin (2010).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Verified Systems International GmbHBremenGermany
  2. 2.Department of Mathematics and Computer ScienceUniversity of BremenBremenGermany

Personalised recommendations