Abstract
The use of formal methods for verification and validation of critical and complex systems is important, but can be extremely tedious without modularisation mechanisms. SysML/KAOS is a requirements engineering method. It includes a goal modeling language to model requirements from stakeholder’s needs. It also contains a domain modeling language for the representation of system application domain using ontologies. Translation rules have been defined to automatically map SysML/KAOS models into B System specifications. Moreover, since the systems we are interested in naturally break down into subsystems (enabling the distribution of work between several agents: hardware, software and human), SysML/KAOS goal models allow the capture of assignments of requirements to agents responsible of their achievement. Each agent is associated with a subsystem. The contribution of this paper is an approach to ensure that a requirement assigned to a subsystem is well achieved by the subsystem. A particular emphasis is placed on ensuring that system invariants persist in subsystems specifications.
French National Research Agency (ANR).
Natural Sciences and Engineering Research Council of Canada (NSERC).
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.
- 2.
The before-after predicate of \(E_1\) denotes the relationship holding between the state variable of machine \(M_1\) just before (denoted by \(x_1\)) and after (denoted by \(x_1'\)) the triggering of \(E_1\) [2].
- 3.
For an event G, G_Guard represents the guard of G and G_Post represents the post condition of its actions [24].
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundamenta Informaticae 77(1–2), 1–28 (2007)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM (JACM) 49(5), 672–713 (2002)
ANR-14-CE28-0009: Formose ANR project (2017). http://formose.lacl.fr/
Bauer, J.C.: Specification for a software program for a boiler water content monitor and control system. Institute of Risk Research, University of Waterloo (1993)
Butler, M.: Synchronisation-based decomposition for Event-B. RODIN Deliverable D19 Intermediate report on methodology, pp. 47–57 (2006)
Butler, M.: An approach to the design of distributed systems with B AMN. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 221–241. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0027291
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
Claassen, A.F., Lathon, R.D., Rochowiak, D.M., Interrante, L.D.: Active rescheduling for goal maintenance in dynamic manufacturing-systems. In: Proceedings of the AAAI Spring Symposium (1994)
ClearSy: Atelier B: B System (2014). http://clearsy.com/
Davis, W.J.: Evaluating performance of distributed intelligent control systems. NIST Special Publication SP, pp. 225–232 (2001)
Tueno Fotso, S.J., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 262–276. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_18
Tueno Fotso, S.J., Mammar, A., Laleau, R., Frappier, M.: Event-B expression and verification of translation rules between SysML/KAOS domain models and B system specifications. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 55–70. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_5
Goranko, V.: Coalition games and alternating temporal logics. In: Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge, pp. 259–272. Morgan Kaufmann Publishers Inc. (2001)
Hause, M., et al.: The SysML modelling language. In: Fifteenth European Systems Engineering Conference, vol. 9. Citeseer (2006)
Van der Hoek, W., Wooldridge, M.: Multi-agent systems. Found. Artif. Intell. 3, 887–928 (2008)
Iliasov, A., et al.: Supporting reuse in Event B development: modularisation approach. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 174–188. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_14
Laleau, R., Semmak, F., Matoussi, A., Petit, D., Hammad, A., Tatibouet, B.: A first attempt to combine SysML requirements diagrams and B. Innov. Syst. Softw. Eng. 6(1–2), 47–54 (2010)
van Lamsweerde, A.: Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley (2009)
Lecomte, T., Deharbe, D., Prun, E., Mottin, E.: Applying a formal method in industry: a 25-year trajectory. In: Cavalheiro, S., Fiadeiro, J. (eds.) SBMF 2017. LNCS, vol. 10623, pp. 70–87. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70848-5_6
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.: Building abstract formal Specifications driven by goals. Ph.D. thesis, University of Paris-Est, France (2011). https://tel.archives-ouvertes.fr/tel-00680736
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
Openflexo: Openflexo project (2018). https://github.com/openflexo-team/
Parnas, D.L., Madey, J.: Functional documents for computer systems. Sci. Comput. Program. 25(1), 41–61 (1995)
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
Sengupta, K., Hitzler, P.: Web ontology language (OWL). In: Encyclopedia of Social Network Analysis and Mining, pp. 2374–2378 (2014)
Silva, R.: Towards the composition of specifications in Event-B. Electron. Notes Theor. Comput. Sci. 280, 81–93 (2011)
Silva, R., Butler, M.J.: Shared event composition/decomposition in Event-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 122–141. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_7
Silva, R., Pascal, C., Hoang, T.S., Butler, M.J.: Decomposition tool for Event-B. Softw. Pract. Exper. 41(2), 199–208 (2011)
Suski, G., et al.: The nova control system-goals, architecture, and system design. In: Distributed Computer Control Systems 1982, pp. 45–56. Elsevier (1983)
Tan, J.K.: Health management information systems: methods and practical applications. Jones & Bartlett Learning (2001)
Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Towards using ontologies for domain modeling within the SysML/KAOS approach. In: RE Workshops, pp. 1–5. IEEE Computer Society (2017)
Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Formal Representation of SysML/KAOS Domain Models. ArXiv e-prints, cs.SE, 1712.07406, December 2017. https://arxiv.org/pdf/1712.07406.pdf
Tueno, S., Laleau, R., Mammar, A., Frappier, M.: The SysML/KAOS Domain Modeling Approach. ArXiv e-prints, cs.SE, 1710.00903, September 2017. https://arxiv.org/pdf/1710.00903.pdf
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
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 Nature Switzerland AG
About this paper
Cite this paper
Tueno Fotso, S.J., Frappier, M., Laleau, R., Mammar, A., Leuschel, M. (2018). Formalisation of SysML/KAOS Goal Assignments with B System Component Decompositions. In: Furia, C., Winter, K. (eds) Integrated Formal Methods. IFM 2018. Lecture Notes in Computer Science(), vol 11023. Springer, Cham. https://doi.org/10.1007/978-3-319-98938-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-98938-9_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98937-2
Online ISBN: 978-3-319-98938-9
eBook Packages: Computer ScienceComputer Science (R0)