November 16, 2020
Régine Laleau (LACL)En ingénierie des exigences (IE) pour les systèmes critiques, au moins deux types de modèles sont nécessaires.
D’une part les exigences doivent être exprimées dans un langage qui puisse être compris par les différentes parties-prenantes qui participent à la construction du modèle d’exigences dans un but de validation. Dans la plupart des méthodes d’IE ce langage est graphique.
D’autre part, il faut un langage formel pour vérifier les exigences critiques. Le projet ANR FORMOSE avait pour objectif de construire une méthode formelle d’IE orientée modèles pour des systèmes critiques.
Nous avons développé une méthode d’IE orientée buts, SysML/KAOS, qui permet de décrire graphiquement les exigences à différents niveaux d’abstraction. Ce modèle des exigences est complété par un modèle de domaine pour décrire les entités du système et leurs propriétés. A partir de ces deux modèles, une spécification formelle Event-B est alors dérivée. Pour maintenir la cohérence entre les deux modèles graphique et formel, nous avons utilisé une technique de fédération de modèles qui consiste à définir un méta-modèle pour chacun des langages puis un modèle d’alignement qui permet de spécifier des liens dynamiques entre les deux méta-modèles. L’approche a été implémentée sur l’outil Openflexo.