  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.
