Towards the qualification of an AADL model transformation tool with contracts

Abstract

Model-Based Engineering (MBE) can be used to build complex and critical systems. At the core of MBE, model transformation allows for the automatic processing of models to automatically generate code of the application or to perform analysis. In the context of safety-critical applications, qualification of MBE tools must provide evidence that the model transformation process is ``correct''. Its implementation must (i) document the transformation process itself, and support validation (ii) to infer properties on this process. We propose to use contracts to support qualification of the model transformation process. Contracts, by providing a formal specification of a model transformation, can be used in different ways, either to detect contract violations at run time or to demonstrate properties of the model transformation at the design time. This approach has been experimented in the context of Ocarina, an AADL toolset (Architecture Analysis and Design Language).