Towards a tooled and proven formal requirements engineering approach

Vers une approche formelle d'ingénierie des exigences outillée et éprouvée La méthode SysML/KAOS permet de modéliser les exigences d’un système sous forme d’hiérarchies de buts. B System est une méthode formelle qui permet de construire, vérifier et valider la spécification d’un système. Un modèle B System est constitué d’une partie structurelle (ensembles abstraits et énumérés, constantes et leurs propriétés, et variables et leur invariant) et d’une partie comportementale (évènements). Lors de travaux antérieurs, des liens de correspondance ont été établis entre SysML/KAOS et B System afin de produire une spécification formelle à partir de la modélisation des exigences. Cette spécification sert de base pour les tâches de vérification et de validation formelle afin de détecter et corriger les potentielles erreurs de spécification. Toutefois, il est nécessaire de fournir manuellement la partie structurelle du modèle B System.L’objectif de cette thèse est d’enrichir SysML/KAOS avec un langage permettant de modéliser le domaine du système et qui serait compatible avec le langage de modélisation des exigences. Ceci inclut non seulement la définition du langage, mais aussi des mécanismes permettant d’exploiter la modélisation du domaine pour fournir la partie structurelle de la spécification B System issue de la formalisation des exigences. Le langage défini exploite la notion d’ontologie pour permettre la représentation formelle du domaine. Bien plus, les liens et règles de correspondance établis et formellement vérifiés permettent tant la propagation que la rétropropagation des ajouts et suppressions, entre modèles de domaine et spécifications B System. Un autre aspect essentiel de la thèse réside dans l’évaluation de la méthode SysML/KAOS sur des études de cas. Par ailleurs, les systèmes, au vu de leur complexité, se doivent d’être décomposés en sous-systèmes. La thèse décrit en conséquence des mécanismes permettant de garantir formellement que chaque exigence affectée à un sous-système sera bien satisfaite par ce dernier, dans la limite définie par la spécification du système et des sous-systèmes.La méthode SysML/KAOS, ainsi enrichie, a été implémentée au sein d’un outil libre en utilisant la plateforme de fédération de modèles Openflexo, et a été évaluée sur différentes études de cas d’envergure industrielle. Elle permet la vérification formelle des exigences et facilite leur validation par des parties prenantes non spécialistes de méthodes formelles. Toutefois, les tâches de spécification des formules logiquesdu modèle de domaine, qui donnent lieu aux propriétés et invariants du modèle BSystem, et du corps des évènements B System, ainsi que les tâches de vérification etvalidation formelles sont coûteuses en temps et nécessitent l’implication d’expertsen méthodes formelles. Il s’agit là du prix à payer pour des exigences formellementcorrectes.