English

SysML/KAOS Domain Models and B System Specifications

Software Engineering 2018-07-02 v4

Abstract

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.

Cite

@article{arxiv.1803.01972,
  title  = {SysML/KAOS Domain Models and B System Specifications},
  author = {Steve Jeffrey Tueno Fotso and Marc Frappier and Amel Mammar and Régine Laleau},
  journal= {arXiv preprint arXiv:1803.01972},
  year   = {2018}
}

Comments

arXiv admin note: text overlap with arXiv:1712.07406

R2 v1 2026-06-23T00:43:12.109Z