Verifying Functional Behaviors of Automotive Products in EAST-ADL2 Using UPPAAL-PORT

  • Eun-Young Kang
  • Pierre-Yves Schobbens
  • Paul Pettersson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6894)


We study the use of formal modeling and verification techniques at an early stage in the development of safety-critical automotive products which are originally described in the domain specific architectural language EAST-ADL2. This architectural language only focuses on the structural definition of functional blocks. However, the behavior inside each functional block is not specified and that limits formal modeling and analysis of systems behaviors as well as efficient verification of safety properties. In this paper, we tackle this problem by proposing one modeling approach, which formally captures the behavioral execution inside each functional block and their interactions, and helps to improve the formal modeling and verification capability of EAST-ADL2: the behavior of each elementary function of EAST-ADL2 is specified in UPPAAL Timed Automata. The formal syntax and semantics are defined in order to specify the behavior model inside EAST-ADL2 and their interactions. A composition of the functional behaviors is considered a network of Timed Automata that enables us to verify behaviors of the entire system using the UPPAAL model checker. The method has been demonstrated by verifying the safety of the Brake-by-wire system design.


Model Checker Functional Block Functional Behavior Automotive Product Time Automaton 
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.
    Advancing Traffic Efficiency and Safety through Software Technology Phase 2, European project (2010),
  2. 2.
    AUTomotive Open System Architecture (2010),
  3. 3.
    Carlson, J., Håkansson, J., Pettersson, P.: SaveCCM: An analysable component model for real-time systems. In: Liu, Z., Barbosa, L. (eds.) Proceedings of the 2nd Workshop on Formal Aspects of Components Software (FACS 2005). Electronic Notes in Theoretical Computer Science, vol. 160, pp. 127–140. Elsevier, Amsterdam (2006)Google Scholar
  4. 4.
    David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed i/o automata: a complete specification theory for real-time systems. Hybrid Systems, 91–100 (2010)Google Scholar
  5. 5.
    Feng, L., Chen, D., Lönn, H., Törngren, M.: Verifying system behaviors in east-adl2 with the SPIN model checker. In: IEEE International Conference on Mechatronics and Automation, Xi’an China (August 2011)Google Scholar
  6. 6.
    Grimm, K.: Software technology in an automotive company - major challenges. In: International Conference on Software Engineering, p. 498 (2003)Google Scholar
  7. 7.
    Håkansson, J.: Design and verification of component based real-time systems. PhD thesis, Uppsala University (2009)Google Scholar
  8. 8.
    Håkansson, J., Carlson, J., Monot, A., Pettersson, P., Slutej, D.: Component-based design and analysis of embedded systems with UPPAAL PORT. In: Cha, S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 252–257. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gear controller. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 281–297. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Jerson Ortiz, J., Legay, A., Schobbens, P.-Y.: Memory event clocks. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 198–212. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  11. 11.
    Open Source Tool for Graphical UML2 Modeling (2010),
  12. 12.
    Raskin, J.-F., Schobbens, P.-Y.: State clock logic: A decidable real-time logic. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 33–47. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Rumbaugh, J., Jacobson, I.: United Modeling Language User Guide, 2nd edn. Addison-Wesley, Reading (1998)Google Scholar
  14. 14.
    Sandberg, A., Chen, D., Lönn, H., Johansson, R., Feng, L., Törngren, M., Torchiaro, S., Tavakoli-Kolagari, R., Abele, A.: Model-based safety engineering of interdependent functions in automotive vehicles using EAST-ADL2. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 332–346. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Sangiovanni-Vincentelli, A., Di Natale, M.: Embedded system design for automotive applications. Computer 40(10), 42–51 (2007)CrossRefGoogle Scholar
  16. 16.
    SAVE-IDE project at source net,
  17. 17.
    Sentilles, S., Håkansson, J., Pettersson, P., Crnkovic, I.: SAVE-IDE, an integrated development environment for building predictable component-based embedded systems. In: Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2008 (September 2008)Google Scholar
  18. 18.
    Suryadevara, J., Kang, E.-Y., Seceleanu, C., Pettersson, P.: Bridging the semantic gap between abstract models of embedded systems. In: Grunske, L., Reussner, R., Plasil, F. (eds.) CBSE 2010. LNCS, vol. 6092, pp. 55–73. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Eun-Young Kang
    • 1
    • 2
  • Pierre-Yves Schobbens
    • 1
  • Paul Pettersson
    • 2
  1. 1.Computer Science FacultyUniversity of NamurBelgium
  2. 2.MDH PROGRESS Research CentreVästeråsSweden

Personalised recommendations