Towards a tool-supported and proven formal requirements engineering method

The SysML/KAOS method allows to model system requirements through goal hierarchies. B System is a formal method used to construct, verify and validate system specifications. A B System model consists of a structural part (abstract and enumerated sets, constants with their associated properties, and variables with their associated invariant) and a behavioral part (events). Correspondence links are established in previous work between SysML/KAOS and B System to produce a formal specification from requirements models. This specification serves as a basis for formal verification and validation tasks to detect and correct inconsistencies. However, it is required to manually provide the structural part of the B System specification. This thesis aims at enriching SysML/KAOS with a language that allows to model the application domain of the system and which would be compatible with the requirements modeling language. This includes the definition of the domain modeling language and of mechanisms for leveraging domain modeling to provide the structural part of the B System specification obtained from requirements models. The defined language uses ontologies to allow the formal representation of system domain. Moreover, the established correspondence links and rules, formally verified, allow both propagation and backpropagation of additions and deletions, between domain models and B System specifications. An important part of the thesis is also devoted to assessment of the SysML/KAOS method on case studies. Furthermore, since the systems naturally break down into subsystems (enabling the distribution of work between several agents: hardware, software and human), SysML/KAOS goal models allow the capture of assignments of requirements to subsystems responsible of their achievement. This thesis therefore describes the mechanisms required to formally guarantee that each requirement assigned to a subsystem will be well achieved by the subsystem, within the constraints defined by the high-level system and subsystem specifications. The SysML/KAOS method, thus enriched, has been implemented within an opensource tool using the model federation platform Openflexo, and has been evaluated on various industrial scale case studies. It enables the formal verification of requirements and facilitates their validation by the various stakeholders, including those with less or no expertise in formal methods. However, both the specification of the body of B System events and domain model logical formulas (that give B System properties and invariants) and the formal assessment (verification and validation) of the specification can only be manual. They are time consuming and require experts in formal methods. But this is the price to pay to achieve a formal verification and validation of requirements.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 logiques du modèle de domaine, qui donnent lieu aux propriétés et invariants du modèle B System, et du corps des évènements B System, ainsi que les tâches de vérification et validation formelles sont coûteuses en temps et nécessitent l’implication d’experts en méthodes formelles. Il s’agit là du prix à payer pour des exigences formellement correctes