Formal Representation of SysML/KAOS Domain Model (Complete Version)

TL;DR

This paper presents a set of rules to automatically translate SysML/KAOS domain ontologies into Event-B specifications, facilitating formal validation of system requirements for complex systems.

Contribution

It introduces a formal, verified translation method from SysML/KAOS domain models to Event-B, enabling automatic generation of system structure specifications.

Findings

Rules verified using the Rodin tool

Applied to a landing gear system case study

Enables automatic, formal consistency validation

Abstract

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.