@inproceedings{c15f7dcb31e04ef6bb42b1935fa37899,
title = "Formal semantics and verification of AADL modes in timed abstract state machine",
abstract = "AADL (Architectural Analysis \& Design Language) is an architecture description language standard for embedded real-time systems, and it is widely used in aerospace and other safety-critical applications. However, the AADL standard lacks at present a formal semantics. This paper proposes a formal semantics and a verification framework of AADL models with regard to mode change. The precise semantics of AADL mode change protocol is defined by a translation into the TASM (Timed Abstract State Machine) formalism. Then the translational semantics is automated in the AADL2TASM tool, which provides model checking and simulation for AADL models. Finally, the approach is validated with a case study of an automotive cruise control system.",
keywords = "AADL, Mode change, Model transformation, TASM, Translational semantics",
author = "Zhibin Yang and Kai Hu and Dianfu Ma and Lei Pi and Bodeveix, \{Jean Paul\}",
year = "2010",
doi = "10.1109/PIC.2010.5687996",
language = "英语",
isbn = "9781424467860",
series = "Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010",
pages = "1098--1103",
booktitle = "Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010",
note = "2010 1st IEEE International Conference on Progress in Informatics and Computing, PIC 2010 ; Conference date: 10-12-2010 Through 12-12-2010",
}