  In this paper, we use a combination of the SysML/KAOS requirements
engineering method, an extension of SysML, with concepts of the KAOS goal
model, and of the B System formal method. Translation rules from a SysML/KAOS
goal model to a B System specification have been defined. They allow to obtain
a skeleton of the B System specification. To complete it, we have defined a
language to express the domain model associated to the goal model. The
translation of this domain model gives the structural part of the B System
specification. The contribution of this paper is the description of translation
rules from SysML/KAOS domain models to B System specifications. We also present
the formal verification of these rules and we describe an open source tool that
implements the languages and the rules. Finally, we provide a review of the
application of the SysML/KAOS method on case studies such as for the formal
specification of the hybrid ERTMS/ETCS level 3 standard.
