Formal semantics and verification of AADL modes in timed abstract state machine

Zhibin Yang; Kai Hu; Dianfu Ma; Lei Pi; Jean Paul Bodeveix

doi:10.1109/PIC.2010.5687996

Formal semantics and verification of AADL modes in timed abstract state machine

Zhibin Yang^*
, Kai Hu
, Dianfu Ma
, Lei Pi
, Jean Paul Bodeveix

^*Corresponding author for this work

School of Computer Science and Engineering

Beihang University
Université de Toulouse

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

8 Scopus citations

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.

Original language	English
Title of host publication	Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010
Pages	1098-1103
Number of pages	6
DOIs	https://doi.org/10.1109/PIC.2010.5687996
State	Published - 2010
Event	2010 1st IEEE International Conference on Progress in Informatics and Computing, PIC 2010 - Shanghai, China Duration: 10 Dec 2010 → 12 Dec 2010

Publication series

Name	Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010
Volume	2

Conference

Conference	2010 1st IEEE International Conference on Progress in Informatics and Computing, PIC 2010
Country/Territory	China
City	Shanghai
Period	10/12/10 → 12/12/10

Keywords

AADL
Mode change
Model transformation
TASM
Translational semantics

Access to Document

10.1109/PIC.2010.5687996

Cite this

Yang, Z., Hu, K., Ma, D., Pi, L., & Bodeveix, J. P. (2010). Formal semantics and verification of AADL modes in timed abstract state machine. In Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010 (pp. 1098-1103). Article 5687996 (Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010; Vol. 2). https://doi.org/10.1109/PIC.2010.5687996

@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",

}

Yang, Z, Hu, K , Ma, D, Pi, L & Bodeveix, JP 2010, Formal semantics and verification of AADL modes in timed abstract state machine. in Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010., 5687996, Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010, vol. 2, pp. 1098-1103, 2010 1st IEEE International Conference on Progress in Informatics and Computing, PIC 2010, Shanghai, China, 10/12/10. https://doi.org/10.1109/PIC.2010.5687996

Formal semantics and verification of AADL modes in timed abstract state machine. / Yang, Zhibin; Hu, Kai ; Ma, Dianfu et al.
Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010. 2010. p. 1098-1103 5687996 (Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010; Vol. 2).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formal semantics and verification of AADL modes in timed abstract state machine

AU - Yang, Zhibin

AU - Hu, Kai

AU - Ma, Dianfu

AU - Pi, Lei

AU - Bodeveix, Jean Paul

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

KW - AADL

KW - Mode change

KW - Model transformation

KW - TASM

KW - Translational semantics

UR - https://www.scopus.com/pages/publications/79951471687

U2 - 10.1109/PIC.2010.5687996

DO - 10.1109/PIC.2010.5687996

M3 - 会议稿件

AN - SCOPUS:79951471687

SN - 9781424467860

T3 - Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010

SP - 1098

EP - 1103

BT - Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010

T2 - 2010 1st IEEE International Conference on Progress in Informatics and Computing, PIC 2010

Y2 - 10 December 2010 through 12 December 2010

ER -

Yang Z, Hu K , Ma D, Pi L, Bodeveix JP. Formal semantics and verification of AADL modes in timed abstract state machine. In Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010. 2010. p. 1098-1103. 5687996. (Proceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010). doi: 10.1109/PIC.2010.5687996

Formal semantics and verification of AADL modes in timed abstract state machine

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this