AADL Execution Semantics Transformation for Formal Verification

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.