AADL Execution Semantics Transformation for Formal Verification

Author

Abdoul, Thomas ; Champeau, Joël ; Dhaussy, Philippe ; Pillain, Pierre-Yves ; Roger, Jean-Charles

Author_Institution

Lab. DTN, Brest

fYear

2008

fDate

March 31 2008-April 3 2008

Firstpage

263

Lastpage

268

Abstract

The paper presents an AADL model transformation. This transformation provides a formal model for model checking activities. This transformation covers three aspects: structure, behaviour description and execution semantics. The necessity to complete AADL metamodel is shown in order to improve system behaviour. Transformation rules take into account these aspects. The Kermeta metamodeling platform is used to implement these rules which are applied to a case study. In conclusion, we suggest that model transformation provides useful support to improve the integration of formal verification in an industrial engineering process.

Keywords

formal verification; specification languages; AADL execution semantics transformation; AADL metamodel; Kermeta metamodeling platform; behaviour description; formal model; formal verification; industrial engineering process; model checking; model transformation; Automata; Automotive engineering; Delay; Disruption tolerant networking; Formal languages; Formal verification; Metamodeling; Model driven engineering; Power system modeling; Yarn; Model transformation; finite-state verification.; formal checking; metamodel; semantics;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Complex Computer Systems, 2008. ICECCS 2008. 13th IEEE International Conference on

Conference_Location

Belfast

Print_ISBN

0-7695-3139-3

Type

conf

DOI

10.1109/ICECCS.2008.24

Filename

4492901