Yang, Zhibin and Hu, Kai and Zhao, Yong-Wang and Ma, Dianfu and Bodeveix, Jean-Paul Verification of AADL Models with Timed Abstract State Machines. (2015) Journal of Software, 26 (2). 202-222. ISSN 1000-9825
|
(Document in Chinese)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 752kB |
Abstract
This paper presents a formal verification method for AADL (architecture analysis and design language) models by TASM (timed abstract state machine) translation. The abstract syntax of the chosen subset of AADL and of TASM are given. The translation rules are defined clearly by the semantic functions expressed in a ML-like language. Furthermore, the translation is implemented in the model transformation tool AADL2TASM, which provides model checking and simulation for AADL models. Finally, a case study of space GNC (guidance, navigation and control) system is provided.
| Item Type: | Article |
|---|---|
| Additional Information: | Thanks to Chinese Academy of Sciences editor. The definitive version is available at http://www.jos.org.cn/ The original PDF of the article can be found at Chemical Physics Letters website : http://www.jos.org.cn/1000-9825/4776.htm |
| HAL Id: | hal-01153717 |
| Audience (journal): | National peer-reviewed journal |
| Uncontrolled Keywords: | |
| Institution: | French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) Other partners > Beihang University (CHINA) |
| Laboratory name: | |
| Statistics: | download |
| Deposited On: | 02 Feb 2015 16:06 |
Repository Staff Only: item control page
