Event-B Expression and Verification of Translation Rules Between SysML/KAOS Domain Models and B System Specifications

Steve Jeffrey Tueno Fotso, Amel Mammar, Régine Laleau, Marc Frappier
Digital Printed Abstract View Cite
Type
Conference paper
Publication
6th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'18)

Abstract

This paper is about the extension of the SysML/KAOS requirements engineering method with domain models expressed as ontologies. More precisely, it concerns the translation of these ontologies into B System for system construction. The contributions of this paper are twofold. The first one is a formal semantics for the ontology modeling language. The second one is the formal definition of translation rules between ontologies and B system specifications in order to provide the structural part of the formal specification. These translation rules are modeled in Event-B. Their consistency and completeness are proved using Rodin. We show that they are structure preserving (two related elements within the source model remain related within the target model), by proving various isomorphisms between the ontology and the B System specification.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{FotsoMLF18,
  author       = {Steve Jeffrey Tueno Fotso and
                  Amel Mammar and
                  R{\'{e}}gine Laleau and
                  Marc Frappier},
  editor       = {Michael J. Butler and
                  Alexander Raschke and
                  Thai Son Hoang and
                  Klaus Reichl},
  title        = {Event-B Expression and Verification of Translation Rules Between SysML/KAOS
                  Domain Models and {B} System Specifications},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
                  Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10817},
  pages        = {55--70},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-91271-4\_5},
  doi          = {10.1007/978-3-319-91271-4\_5},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/FotsoMLF18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'18

Related