From SysML/KAOS Domain Models to B System Specifications
share
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 goal model to a B System specification have been defined. They allow to obtain a skeleton of the formal 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 formal specification. The contribution of this paper is the description of these rules. 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 approach on case studies such as for the formal specification of the hybrid ERTMS/ETCS level 3 standard.
READ FULL TEXT