Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10817))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The full list can be found in [26].

  2. 2.

    Some guards and actions have been removed for the sake of concision.

References

  1. Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  2. Alkhammash, E., Butler, M.J., Fathabadi, A.S., Cîrstea, C.: Building traceable Event-B models from requirements. Sci. Comput. Program. 111, 318–338 (2015)

    Article  Google Scholar 

  3. Alkhammash, Eman H.: Derivation of Event-B models from OWL ontologies. In: MATEC Web Conference, vol. 76, p. 04008 (2016)

    Article  Google Scholar 

  4. Ameur, Y.A., Baron, M., Bellatreche, L., Jean, S., Sardet, E.: Ontologies in engineering: the OntoDB/OntoQL platform. Soft. Comput. 21(2), 369–389 (2017)

    Article  Google Scholar 

  5. ANR-14-CE28-0009: Formose ANR project (2017)

    Google Scholar 

  6. Bjørner, D., Eir, A.: Compositionality: ontology and mereology of domains. In: Dams, D., Hannemann, U., Steffen, M. (eds.) Concurrency, Compositionality, and Correctness. LNCS, vol. 5930, pp. 22–59. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11512-7_3

    Chapter  MATH  Google Scholar 

  7. Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1–18. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07512-9_1

    Chapter  Google Scholar 

  8. Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.): Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157. Springer, Heidelberg (2006). https://doi.org/10.1007/11916246

    Book  Google Scholar 

  9. ClearSy: Atelier B: B System (2014). http://clearsy.com/

  10. Dong, J.S., Sun, J., Wang, H.: Z approach to semantic web. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 156–167. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36103-0_18

    Chapter  Google Scholar 

  11. Gnaho, C., Semmak, F., Laleau, R.: Modeling the impact of non-functional requirements on functional requirements. In: Parsons, J., Chiu, D. (eds.) ER 2013. LNCS, vol. 8697, pp. 59–67. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-14139-8_8

    Chapter  Google Scholar 

  12. Hoang, T.S., Butler, M., Reichl, K.: The Hybrid ERTMS/ETCS Level 3 Case Study, pp. 1–3. ABZ (2018)

    Google Scholar 

  13. JetBrains: JetBrains MPS (2017). https://www.jetbrains.com/mps/

  14. Laleau, R., Mammar, A.: An overview of a method and its support tool for generating B specifications from UML notations, pp. 269–272. ICS (2000)

    Google Scholar 

  15. van Lamsweerde, A.: Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley, Hoboken (2009)

    Google Scholar 

  16. Mammar, A., Laleau, R.: On the use of domain and system knowledge modeling in goal-based Event-B specifications. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 325–339. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_23

    Chapter  Google Scholar 

  17. Matoussi, A., Gervais, F., Laleau, R.: A goal-based approach to guide the design of an abstract Event-B specification. In: ICECCS 2011, pp. 139–148. IEEE Computer Society (2011)

    Google Scholar 

  18. OpenFlexo: OpenFlexo project (2015). http://www.openflexo.org

  19. Pierra, G.: The PLIB ontology-based approach to data integration. In: Jacquart, R. (ed.) Building the Information Society. IIFIP, vol. 156, pp. 13–18. Springer, Boston, MA (2004). https://doi.org/10.1007/978-1-4020-8157-6_2

    Chapter  Google Scholar 

  20. Project, D.: Rodin Atelier B Provers Plug-in (2017). https://www3.hhu.de/stups/handbook/rodin/current/html/atelier_b_provers.html

  21. Sengupta, K., Hitzler, P.: Web ontology language (OWL). In: Encyclopedia of Social Network Analysis and Mining, pp. 2374–2378 (2014)

    Google Scholar 

  22. Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)

    Article  Google Scholar 

  23. SYSTEREL: Rodin SMT Solvers Plug-in (2017). http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in

  24. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Towards using ontologies for domain modeling within the SysML/KAOS approach. In: 25th IEEE International Requirements Engineering Conference on IEEE Proceedings of MoDRE Workshop (2017)

    Google Scholar 

  25. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Event-B Specification of Translation Rules (2017). https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser/tree/master/SysMLKAOSDomainModelRules

  26. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Formal Representation of SysML/KAOS Domain Models. ArXiv e-prints, cs.SE, 1712.07406, December 2017

    Google Scholar 

  27. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML/KAOS Domain Modeling Approach. ArXiv e-prints, cs.SE, 1710.00903, September 2017

    Google Scholar 

  28. Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML/KAOS Domain Modeling Language (Tool and Case Studies) (2017). https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser/tree/master

  29. Wang, H.H., Damljanovic, D., Sun, J.: Enhanced semantic access to formal software models. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 237–252. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16901-4_17

    Chapter  Google Scholar 

Download references

Acknowledgment

This work is carried out within the framework of the FORMOSE project [5] funded by the French National Research Agency (ANR). It is also partly supported by the Natural Sciences and Engineering Research Council of Canada (NSERC).

Author information

Authors and Affiliations

  1. Université Paris-Est Créteil, LACL, Créteil, France

    Steve Jeffrey Tueno Fotso & Régine Laleau

  2. Télécom SudParis, SAMOVAR-CNRS, Evry, France

    Amel Mammar

  3. Université de Sherbrooke, GRIL, Québec, Canada

    Steve Jeffrey Tueno Fotso & Marc Frappier

Authors
  1. Steve Jeffrey Tueno Fotso
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amel Mammar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Régine Laleau
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marc Frappier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Steve Jeffrey Tueno Fotso .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Universität Ulm, Ulm, Germany

    Alexander Raschke

  3. University of Southampton, Southampton, United Kingdom

    Thai Son Hoang

  4. Thales Austria GmbH, Vienna, Austria

    Klaus Reichl

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Tueno Fotso, S.J., Mammar, A., Laleau, R., Frappier, M. (2018). Event-B Expression and Verification of Translation Rules Between SysML/KAOS Domain Models and B System Specifications. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-91271-4_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-91270-7

  • Online ISBN: 978-3-319-91271-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation