Formally Tracing Executions From an Analysis Tool Back to a Domain Specific Modeling Language's Operational Semantics

The increasing complexity of software development requires rigorously defined domain specific modelling languages (DSML). Model-driven engineering (MDE) allows users to define their language's syntax in terms of metamodels. Several approaches for defining operational semantics of DSML have also been proposed. These approaches allow, in principle, for model execution and for formal analyses of the DSML. However, most of the time, the executions/analyses are performed via transformations to other languages: code generation, resp. translation to the input language of a model checker. The consequence is that the results (e.g., a program crash log, or a counterexample returned by a model checker) may not be straightforward to interpret by the users of a DSML. In this research report, we propose a formal and operational framework for tracing such results back to the original DSML's syntax and operational semantics.Le besoin en définitions rigoureuses de langages de modélisation métiers (LMM) croît avec la complexité du développement logiciel. L'ingénierie dirigée par les modèles (IDM), permet à des utilisateurs de définir la syntaxe de nouveaux langages à l'aide de metamodèles. Quelques approches proposent également des façons de définir la sémantique opérationnelle de ces langages. Ces approches permettent, en principe, l'exécution des programmes (modèles) et leur analyse formelle. Cependant, la plupart du temps, les analyses sont réalisées à l'aide de transformations de ces modèles vers d'autres langages, pour être exécutés (langages généralistes, type C par exemple) ou vérifiés (langages d'entrées de model checkers, de simulateurs, ...). En conséquence, ces résultats (un log de crash de programme, une exécution contre exemple provenant de la vérification d'une propriété par un model-checker, par exemple) peuvent ne pas être directement compréhensibles par les utilisateurs d'un LMM. Dans ce rapport, nous proposons une méthode formelle et opérationnelle pour exprimer ces exécutions en terme de syntaxe et sémantique du LMM initial