Title :
Verifying system behaviors in EAST-ADL2 with the SPIN model checker
Author :
Feng, Lei ; Chen, DeJiu ; Lönn, Henrik ; Törngren, Martin
Author_Institution :
Dept. of Machine Design, R. Inst. of Technol. - KTH, Stockholm, Sweden
Abstract :
EAST-ADL2 is a domain-specific architecture description language to support the model-based development of automotive embedded systems. It emerged to manage the complexity of software and electronics in advanced automotive applications. The language focuses on the structural definition for functional specifications. Behavior is defined only on the component level, in terms of functional blocks and their triggers and interfaces. The behavioral definition inside each functional block is not prescribed. This paper shows one approach to augment the language with precise syntax and semantics for behavior, and develops a procedure that transforms the composed behavioral model to the SPIN model for logic model checking. The contribution improves the modeling and verification capability of EAST-ADL2.
Keywords :
automotive engineering; embedded systems; program verification; specification languages; EAST-ADL2; SPIN model checker; automotive embedded systems; domain specific architecture description language; logic model checking; software complexity; system behaviors verification; Analytical models; Computational modeling; Cooperative systems; Semantics; Software; Unified modeling language; Vehicles;
Conference_Titel :
Mechatronics and Automation (ICMA), 2010 International Conference on
Conference_Location :
Xi´an
Print_ISBN :
978-1-4244-5140-1
Electronic_ISBN :
2152-7431
DOI :
10.1109/ICMA.2010.5588261