Verifying Functional Behaviors of Automotive Products in EAST-ADL2 Using UPPAAL-PORT
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.
KeywordsModel Checker Functional Block Functional Behavior Automotive Product Time Automaton
Unable to display preview. Download preview PDF.
- 1.Advancing Traffic Efficiency and Safety through Software Technology Phase 2, European project (2010), http://www.atesst.org
- 2.AUTomotive Open System Architecture (2010), http://www.autosar.org
- 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.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.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.Grimm, K.: Software technology in an automotive company - major challenges. In: International Conference on Software Engineering, p. 498 (2003)Google Scholar
- 7.Håkansson, J.: Design and verification of component based real-time systems. PhD thesis, Uppsala University (2009)Google Scholar
- 11.Open Source Tool for Graphical UML2 Modeling (2010), http://www.papyrusuml.org
- 13.Rumbaugh, J., Jacobson, I.: United Modeling Language User Guide, 2nd edn. Addison-Wesley, Reading (1998)Google Scholar
- 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
- 16.SAVE-IDE project at source net, http://sourceforge.net/projects/save-ide/
- 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