Nos partenaires

CNRS

Rechercher





Accueil du site > Français > Thèmes de recherche > Thème 7 - Sûreté de développement du logiciel > Equipe MACAO > Propositions de stages, thèses et post-doc > Thèses

Un framework générique pour la simulation et l’exploration efficace de l’espace d’états dans le cadre MDA

Contact : Iulian Ober

Laboratoire IRIT — Thème 7 —Equipe MACAO

Direction et unité d’accueil

Iulian Ober (IRIT/MACAO),
  • Institut de Recherche en Informatique de Toulouse (IRIT)
  • Equipe : MACAO

Avec l’utilisation croissante de langages de modélisation spécifiques (domain specific modeling languages, ou DMSLs) ou généralistes (UML, SysML, etc.), l’ingénierie des langages est (re-)devenue une thématique très porteuse, où de nouvelles applications voient constamment le jour. Un problème récurent pour lequel aucune solution satisfaisante n’existe actuellement est celui de la simulation et de l’exploration efficace de l’espace d’états de modèles définis dans ces langages. Si avec les outils actuels il est très aisé de définir la syntaxe et la sémantique statique de ces langages, ou de créer des traducteurs, la situation est toute autre quand il s’agit de la sémantique dynamique et de la construction d’outils de simulation ou model-checking pour des langages non-triviaux.

Il n’existe pas actuellement de technique reconnue pour définir la sémantique opérationnelle de langages de modélisation, ni de technique spécifique pour implanter des moteurs de simulation pour de tels langages. Un début de réponse est apporté en utilisant des transformations endogènes pour la définition du comportement des méta-modèles, e.g. par des transformations de graphes [1,2] ou dans des langages impératifs comme Kermeta [3]. Cependant, outre les problèmes de performance (e.g., impossibilité d’implémenter des structures de données performantes pour le stockage des états), l’utilisation de ce type de méthode pose aussi des problèmes conceptuels. Par exemple, ils ne distinguent pas entre le modèle décrit dans le DSML et le modèle d’exécution, alors que souvent pour des langages non-triviaux un état du système n’a pas la même structure que le modèle (en sémantique opérationnelle, cette distinction est faite entre la syntaxe abstraite d’un programme et la structure des configurations dynamiques).

Pour les langages de programmation textuels, des approches récentes comme K [4] permettent de définir la sémantique opérationnelle sous une forme qui peut être exploitée avec des outils de réécriture de termes comme Maude [5]. Ainsi, un outil de réécriture peut fournir une infrastructure générique pour la construction d’explorateurs de graphes d’états explicites et de model-checkers. L’objectif de la thèse est d’adapter ce type d’approche aux langages de modélisation définis dans le cadre d’une architecture type MDA [6]. Nous nous proposons de restreindre l’étude aux langages dont la sémantique peut être donnée sous forme opérationnelle structurelle (SOS [7]) et dont l’espace d’état, discret, peut être représenté comme un système de transitions étiquetés. La plupart des DSMLs rencontrés dans la littérature rentrent dans cette catégorie. Outre la définition du framework théorique et logiciel, l’objectif sera d’utiliser ce cadre pour des applications de simulation et de vérification de modèles de systèmes embarqués critiques dans le domaine aérospatial, en collaboration avec les partenaires industriels de l’équipe d’accueil.

Profil du candidat

Les candidats doivent être motivés pour travailler dans les domaines du génie logiciel, de l’ingénierie système et des méthodes formelles. Des connaissances de base dans le domaine de la simulation et de la vérification formelle, ainsi que de bonnes capacités d’abstraction et de raisonnement abstrait sont attendues. Un très bon niveau d’anglais ainsi que de bonnes capacités rédactionnelles sont requises.

Contexte de travail

La thèse se déroulera au sein de l’équipe MACAO de l’IRIT, à Toulouse.

Références

[1] José Eduardo Rivera, Francisco Durán, Antonio Vallecillo : Formal Specification and Analysis of Domain Specific Models Using Maude. Simulation 85(11-12) : 778-792 (2009) [2] István Ráth, David Vago, Dániel Varró : Design-time simulation of domain-specific models by incremental pattern matching. VL/HCC 2008 : 219-222 [3] Jean-Marc Jézéquel, Olivier Barais, Franck Fleurey : Model Driven Language Engineering with Kermeta. Generative and Transformational Techniques in Software Engineering III - International Summer School, GTTSE 2009. LNCS 6491. Springer, 2011. [4] Grigore Rosu, Traian-Florin Serbanuta : An overview of the K semantic framework. J. Log. Algebr. Program. 79(6) : 397-434 (2010) [5] José Eduardo Rivera, Francisco Durán, Antonio Vallecillo : Formal Specification and Analysis of Domain Specific Models Using Maude. Simulation 85(11-12) : 778-792 (2009) [6] Object Management Group. MDA Guide Version 1.0.1. http://www.omg.org/cgi-bin/doc?omg/... [7] Plotkin, G. D. : A structural approach to operational semantics. J. Log. Algebr. Program., 60-61:17–139. 2004