Verification of AUTOSAR Software Architectures with Timed Automata

  • Steffen BeringerEmail author
  • Heike Wehrheim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)


Today, automotive software is getting increasingly complex while at the same time development cycles are shortened due to time and cost constraints. For the validation of electronic control unit software, this results in a major challenge. Especially for safety critical software, like automotive software, high quality must be guaranteed. Formal verification of automotive software architecture models enables early verification of safety constraints, before the complete system is assembled and ready for simulation. One option for formal verification of safety critical software is modeling and verification using timed automata. In this paper, we present a method for the verification of AUTOSAR software models by transforming the software architecture as well as the corresponding AUTOSAR timing constraints into timed automata.


Timing Requirement Software Architecture Event Chain Time Automaton Clock Constraint 
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.


  1. 1.
  2. 2.
    Richter, K.: Compositional scheduling analysis using standard event models: the SymTA/S approach. Ph.D. thesis, Braunschweig (2005)Google Scholar
  3. 3.
    Feiertag, N., Richter, K., Nordlander, J., Jonsson, J.: A compositional framework for end-to-end path delay calculation of automotive systems under different path semantics. In: IEEE Real-Time Systems Symposium 2008, vol. 29 (2008)Google Scholar
  4. 4.
    Perathoner, S., Wandeler, E., Thiele, L., Hamann, A., Schliecker, S., Henia, R., Racu, R., Ernst, R., Harbour, M.G.: Influence of different system abstractions on the performance analysis of distributed real-time systems. J. Des. Autom. Embed. Syst. 13(1–2), 27–49 (2009)CrossRefGoogle Scholar
  5. 5.
    Neumann, S., Kluge, N., Wätzoldt, S.: Automatic transformation of abstract autosar architectures to timed automata. In: Proceedings of the 5th International Workshop on Model Based Architecting and Construction of Embedded Systems, ACES-MB 2012, pp. 55–60. ACM, New York (2012)Google Scholar
  6. 6.
    Gehrke, M., Nawratil, P., Niggemann, O., Schäfer, W., Hirsch, M.: Scenario-based verification of automotive software systems. In: Giese, H., Rumpe, B., Schätz, B. (eds.) Dagstuhl-Workshop MBEES. Daghstuhl-Workshop MBEES, vol. 2, pp. 35–42. TU Braunschweig, Institut für Software Systems Engineering (2006)Google Scholar
  7. 7.
    Scheickl, O., Ainhauser, C., Gliwa, P.: Tool support for seamless system development based on autosar timing extensions. In: Embedded Real-Time Software and Systems 2012 (2012)Google Scholar
  8. 8.
    Heckmann, R., Ferdinand, C.: Worst-case execution time prediction by static program analysis. In: Jacquart, R. (ed.) Building the Information Society. IFIP Advances in Information and Communication Technology, vol. 156, pp. 377–383. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
  10. 10.
    Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Olderog, E.R., Dierks, H.: Real-Time Systems: Formal Specification and Automatic Verification (2008)Google Scholar
  12. 12.
    Milner, R.R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Berlin (1980)zbMATHGoogle Scholar
  13. 13.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  15. 15.

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.dSPACE GmbHPaderbornGermany
  2. 2.Paderborn UniversityPaderbornGermany

Personalised recommendations