Skip to Main content Skip to Navigation
Conference papers

Contract-Based Verification of Model Transformations: A Formally Founded Approach

Abstract : In safety-critical applications, using a Model Driven Engineering (MDE) approach requires a high level of trust in its underlying model transformations, the correctness of which should be verified formally. However, such verification remains challenging due to the absence of formal foundations of most model-based frameworks involved in MDE (e.g. AADL, SysML). In this paper, we propose a formally founded environment to verify certain aspects of correctness of model transformations in MDE. First, we define a transformation formally: this involves formalizing input and output models at some level of abstraction, as well as the transformation rules. Then, we extend the formalized transformation with contracts to build a Transition System (TS) representing a lightweight extensible verification environment. Finally, we formulate and verify correctness properties which we reduce, based on the previous steps, to reachability properties over the TS. We show how our approach is implemented in Ocarina, an open-source transformation tool for AADL, and how it applies, for example, to build correct transformations from AADL models to real-time task models in Cheddar ADL.
Document type :
Conference papers
Complete list of metadata
Contributor : Guillaume Brau <>
Submitted on : Wednesday, December 30, 2020 - 1:17:02 PM
Last modification on : Thursday, June 10, 2021 - 3:06:32 AM
Long-term archiving on: : Wednesday, March 31, 2021 - 6:42:52 PM


Files produced by the author(s)


  • HAL Id : hal-03059942, version 1


Guillaume Brau, Mohammed Foughali. Contract-Based Verification of Model Transformations: A Formally Founded Approach. 36th ACM/SIGAPP Symposium On Applied Computing (SAC 2021), Mar 2021, Gwangju (virtual), South Korea. ⟨hal-03059942⟩



Record views


Files downloads