1. Profil
Un étudiant en master dans le cadre d’un stage ou éventuellement pour un travail de fin d’étude en collaboration
2. Description
Le B événementiel (ou Event-B) est une langage de spécification formelle de systèmes basé sur un formalisme de théorie des ensembles. Une notion de raffinement permet de représenter le système à différent niveau de raffinement. Le raisonnement formel est assuré par des preuves hautement automatisée. Un outil de support open-source appelé RODIN est également disponible, de même qu’une extension permettant du model-checking.
Un élément majeur dans la démarche de modélisation est d’être capable d’assurer le passage entre des spécifications informelles (texte naturel, structuré) vers un modèle et d’en gérer la traçabilité). Parmi les méthodes envisageable, l’ingénierie des exigences orientée but est un candidat très intéressant car il permet la structuration des propriétés (buts) d’un systèmes (traduit notamment en invariant pour certains), la représentation des agents responsables de buts particuliers, la représentation des frontières du système. Une méthode particulière appelée KAOS dispose en outre d’un niveau formel et d’une notion formelle de raffinement. Elle est aussi supportée par un environnement appelé Objectiver.
L’objectif du travail est d’étendre, expérimenter et outiller une méthode permettant de gérer le passage et la traçabilité entre le niveau d’exigence informel et les spécifications Event-B sur base de travaux en cours (voir références).
3. Références bibliographiques
A. van Lamsweerde, "Goal-Oriented Requirements Engineering : A Guided Tour" , 5th IEEE International Symposium on Requirements Engineering, Toronto, 2001
B événementiel (ou Event-B)
Outil RODIN.
4. Autres éléments d’information
Concernant le B événementiel, le travail pourra impliquer des contacts avec les partenaires du projets européen DEPLOY dont l’objectif est de déployer la méthodologie outillée dans plusieurs domaines industriels.
