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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The full list can be found in [26].
- 2.
Some guards and actions have been removed for the sake of concision.
References
Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)
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)
Alkhammash, Eman H.: Derivation of Event-B models from OWL ontologies. In: MATEC Web Conference, vol. 76, p. 04008 (2016)
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)
ANR-14-CE28-0009: Formose ANR project (2017)
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
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
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
ClearSy: Atelier B: B System (2014). http://clearsy.com/
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
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
Hoang, T.S., Butler, M., Reichl, K.: The Hybrid ERTMS/ETCS Level 3 Case Study, pp. 1–3. ABZ (2018)
JetBrains: JetBrains MPS (2017). https://www.jetbrains.com/mps/
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)
van Lamsweerde, A.: Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley, Hoboken (2009)
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
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)
OpenFlexo: OpenFlexo project (2015). http://www.openflexo.org
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
Project, D.: Rodin Atelier B Provers Plug-in (2017). https://www3.hhu.de/stups/handbook/rodin/current/html/atelier_b_provers.html
Sengupta, K., Hitzler, P.: Web ontology language (OWL). In: Encyclopedia of Social Network Analysis and Mining, pp. 2374–2378 (2014)
Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)
SYSTEREL: Rodin SMT Solvers Plug-in (2017). http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in
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)
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
Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Formal Representation of SysML/KAOS Domain Models. ArXiv e-prints, cs.SE, 1712.07406, December 2017
Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML/KAOS Domain Modeling Approach. ArXiv e-prints, cs.SE, 1710.00903, September 2017
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
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
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
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)