DocumentCode :
2354874
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
fYear :
2010
fDate :
4-7 Aug. 2010
Firstpage :
144
Lastpage :
149
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Mechatronics and Automation (ICMA), 2010 International Conference on
Conference_Location :
Xi´an
ISSN :
2152-7431
Print_ISBN :
978-1-4244-5140-1
Electronic_ISBN :
2152-7431
Type :
conf
DOI :
10.1109/ICMA.2010.5588261
Filename :
5588261
Link To Document :
بازگشت