Formal Modeling of Automotive Software Requirements by Correctness

Abstract:

Correctly modeling software requirements is one of the grand challenges of current ECU (Electronic control Unit) development. To ensure the correctness of the requirements, formal modeling techniques are usually used because they allow analyzers to simulate, verify and even conduct performance analysis in the requirement level. In this paper, we propose a requirements modeling framework, based on the philosophy of separation of concerns and the formal modeling techniques. The main contributions of this paper are two-fold: (1) We divide a complicated automotive software as several concerns, each of which is modeled by different formal techniques, thus the descriptive complexity of the requirements is decreased, and accordingly the models’ understandability is enhanced; (2) The adoption of formal techniques allows us to simulate the execution of the software and calculate the performance in the early stage of development, therefore the correctness of requirements can be improved.

• Periodical: Applied Mechanics and Materials (Volumes 40-41)
• Pages: 961-967
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.40-41.961
• Online since: November 2010
• Authors: Xiao Jian Liu, Zhi Xue Wang, Xu Qin Yan, Yang Li, Jian Xin Li
• Keywords: Architecture Description Language (ADL), Automotive Software, Model-Driven Development, Requirements Modeling, Timed Automata

References

[1] M. Broy, I. Kruger, A. Pretschner and C. Salzmann. Engineering Automotive Software. Proceedings of THE IEEE. 95(2): 356-373, Febrary (2007).

DOI: 10.1109/jproc.2006.888386

[2] EAST-ADL2: http: /www. atesst. org.

[3] R. Alur and D. L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2): 183-235, (1994).

[4] Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal implementation secrets. In Proc. of 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, (2002).

DOI: 10.1007/3-540-45739-9_1

[5] Feiler, P.H., Gluch, D.P., Hudak, J.J.: The Architecture Analysis and Design Language (AADL): An Introduction. Technical Report CMU/SEI-2006-TN-011, Society of Automotive Engineers (2006).

DOI: 10.21236/ada455842

[6] SAVE Project, http: /www. mrtc. mdh. se/SAVE.

[7] Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. Times – a tool for modelling and implementation of embedded systems. In TACAS 2002, volume 2280 of Lecture Notes in Computer Science, pages 460-464. Springer-Verlag, April (2002).

DOI: 10.1007/3-540-46002-0_32

[8] Davis, R. I., A. Burns, R. J. Bril and J. J. Lukkien (2007). Controller Area Network (CAN) schedulability analysis: Refuted, revisited and revised. Real-Time Syst. 35, 239-272.

DOI: 10.1007/s11241-007-9012-7