Title :
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
fDate :
March 31 2008-April 3 2008
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;
Conference_Titel :
Engineering of Complex Computer Systems, 2008. ICECCS 2008. 13th IEEE International Conference on
Conference_Location :
Belfast
Print_ISBN :
0-7695-3139-3
DOI :
10.1109/ICECCS.2008.24
