Formal Representation of SysML/KAOS Domain Model (Complete Version)
This work addresses the need for automated formal validation in requirements engineering for critical and complex systems, representing an incremental improvement by extending existing methods.
The paper tackles the problem of automatically generating the structural part of Event-B specifications from SysML/KAOS domain ontologies to ensure consistency in requirements engineering for critical systems, proposing a set of rules validated through a case study on a landing gear system.
Nowadays, the usefulness of a formal language for ensuring the consistency of requirements is well established. The work presented here is part of the definition of a formally-grounded, model-based requirements engineering method for critical and complex systems. Requirements are captured through the SysML/KAOS method and the targeted formal specification is written using the Event-B method. Firstly, an Event-B skeleton is produced from the goal hierarchy provided by the SysML/KAOS goal model. This skeleton is then completed in a second step by the Event-B specification obtained from system application domain properties that gives rise to the system structure. Considering that the domain is represented using ontologies through the SysML/KAOS Domain Model method, is it possible to automatically produce the structural part of system Event-B models ? This paper proposes a set of generic rules that translate SysML/KAOS domain ontologies into an Event-B specification. The rules have been expressed, verified and validated through the Rodin tool using the Event-B method. They are illustrated through a case study dealing with a landing gear system. Our proposition makes it possible to automatically obtain, from a representation of the system application domain in the form of ontologies, the structural part of the Event-B specification which will be used to formally validate the consistency of system requirements.