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 > Stages de Master 2

Vérification et réécriture de graphes (08/10/2013)

Contact : Christian Percebois et Hanh Nhi Tran

Laboratoire IRIT — Thème 7 — Equipe MACAO

Direction et unité d’accueil

Contexte

Les graphes permettent de représenter de manière abstraite des structures complexes et semblent bien adaptés aux besoins des techniques de modélisation et de transformation développées en Ingénierie du logiciel Dirigée par les Modèles (IDM). Leur principale vertu réside dans leurs fondements théoriques, autour de travaux relevant de la théorie des catégories ou de la logique.

Plusieurs langages de réécriture ont été proposés, comme AGG, ATOM3, VIATRA2, GrGen.Net, GReAT, GROOVE, etc. Ils se basent en principe sur un jeu de règles déclaratives, faisant intervenir un membre gauche jouant le rôle de filtre par rapport à un graphe source et un membre droit explicitant la transformation souhaitée sur le graphe cible. Ces langages de transformation ont toutefois deux faiblesses :

  • Ils offrent peu de primitives évoluées pour gérer l’ordonnancement des règles, ce qui complique parfois la tâche du concepteur qui doit spécifier des conditions d’applicabilité d’une règle.
  • Ils négligent le processus de vérification qui accompagne celui de la transformation proprement dite, et donc sont assez limités au regard de la spécification des effets de la règle sur le graphe cible. Un nouveau courant de recherche en réécriture de graphes vise à définir un véritable langage de programmation permettant notamment de spécifier finement le contrôle des règles en y intégrant des conditions relatives à leur cohérence. Parmi les travaux de cette tendance, nous nous intéressons plus particulièrement au langage Graph Programming (GP) de l’université de York [1, 2, 3].

Objectif

Ce stage fait partie d’une thématique plus large de raisonnement sur les graphes, abordée dans le projet ANR Blanc CLIMT (Categorical and Logical Methods in Model Transformation) [4]. Au sein de ce projet, nous avons proposé et implémenté quelques techniques de vérification via des assistants de preuve [5, 6] et développé des études de cas de transformations de graphes en utilisant l’outil Henshin [7].

Le stage de Master a pour but de greffer au langage GP des mécanismes de spécification et de vérification de la véracité des règles de transformation. L’approche sera expérimentée sur les études de cas du projet CLIMT.

Les tâches du stage sont les suivantes :

  1. Analyser les études de cas CLIMT :
    • définir l’ordonnancement des règles.
    • identifier les invariants de transformation, ou bien les pré- et post-conditions associées à l’exécution d’une règle ou d’un paquet de règles.
  2. Évaluer :
    • l’expressivité du langage GP vis-à-vis du contrôle de l’ordonnancement des règles.
    • l’expressivité de la logique utilisée dans GP pour exprimer des invariants et des pré- et post-conditions identifiés à l’étape précédente.
  3. À partir des éventuelles lacunes du langage, étudier les différentes logiques et en choisir une qui permette d’exprimer adéquatement des propriétés des études de cas CLIMT à vérifier.
  4. Intégrer au langage GP les opérateurs de la logique choisie à l’étape précédente et programmer dans GP les études de cas CLIMT.

Le sujet de Master trouve naturellement un prolongement en thèse.

Références

  • [1] Detlef Plump. The graph programming language GP. In Proc. Algebraic Informatics (CAI 2009), volume 5725 of Lecture Notes in Computer Science, pages 99–122. Springer-Verlag, 2009.
  • [2] Detlef Plump and Sandra Steinert. The semantics of graph programs. In Proc. Rule-Based Programming (RULE 2009), volume 21 of Electronic Proceedings in Theoretical Computer Science, pages 27–38, 2010.
  • [3] GP. http://www.cs.york.ac.uk/plasma/wik...
  • [4] CLIMT. http://climt.imag.fr/
  • [5] Christian Percebois, Martin Strecker and Hanh Nhi Tran. Rule-level Verification of Graph Transformations for Invariants based on Edges’ Transitive Closure. 11th International Conference on Software Engineering and Formal Methods (SEFM’2013), Madrid, Spain, September 2013.
  • [6] Hanh Nhi Tran and Christian Percebois. Towards a Rule-Level Verification Framework for Property-Preserving Graph Transformations. ICST Workshop on Verification and Validation of Model Transformations (VOLT’2012), Montréal, Canada, April 2012.
  • [7] Henshin. http://www.eclipse.org/henshin/