Contract-Based Verification of Model Transformations: A Formally Founded Approach - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

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

Mohammed Foughali

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (622.07 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03059942 , version 1 (30-12-2020)

Identifiants

  • HAL Id : hal-03059942 , version 1

Citer

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⟩
61 Consultations
22 Téléchargements

Partager

Gmail Facebook X LinkedIn More