Abstract
This paper describes a case study of the SysML/KAOS method for a road transportation system for the City of Montreal (VdM), the second-largest city in Canada. The transportation system was developed from unstructured requirements represented in textual and schematic documents. Therefore, the VdM wanted to investigate new ways of organising and analysing the requirements of traffic projects, in order to increase the level of confidence in their safety, usability and reusability. This paper describes the formal specification, verification and validation of system requirements and provides an appraisal of the SysML/KAOS requirements engineering method on an industrial-scale case study. SysML/KAOS is designed within the ANR FORMOSE project to bridge the gap between stakeholder needs and the formal specification of system functionalities and domain constraints. The method has proven useful to deal with the seven refinement levels, twelve components (human, hardware, software and cyber-physical) and a hundred functional and non-functional goals that constitute the specification of the road transportation system, mainly focused on the safe movement of vehicles on road. It especially facilitated their validation with VdM stakeholders who had never dealt with formal methods and requirements engineering. Animation tools (ProB and B-Motion Studio) were also used to validate the formal specification with VdM stakeholders. This paper also reports improvements identified to enhance the expressiveness of SysML/KAOS goal modeling languages during validation sessions with VdM stakeholders. This includes the introduction of a non-functional goal refinement strategy based on logical formulas and of an obstacle modeling language.
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
Notes
- 1.
Event specification restricted to show only the most relevant part with respect to the one of event BringOutEachVehiclePresentInTunnel. The full version can be found in [1].
- 2.
University Paris Est Créteil; University of Sherbrooke; IMT Brest, France; etc.
- 3.
THALES, France; ClearSy Systems Engineering, France; Openflexo, France.
References
Road transportation system: SysML/KAOS requirements modeling (2018). https://github.com/stuenofotso/SysML_KAOS_Domain_Model_Parser/tree/master/Bonaventure_project
Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, New York (2010)
Abrial, J.R., Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (2005)
ANR-14-CE28-0009: Formose ANR project (2017)
Butler, M.J., 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
Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.): ABZ 2018. LNCS, vol. 10817. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4
ClearSy: Atelier B: B System (2014). http://clearsy.com/
Deploy Project: Rodin Atelier B Provers Plug-in (2017). https://www3.hhu.de
Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Back propagating B system updates on SysML/KAOS domain models. In: ICECCS, pp. 160–169. IEEE (2018)
Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. In: Butler et al. [6], pp. 262–276
Fotso, S.J.T., 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 et al. [6], pp. 55–70
Gnaho, C., Laleau, R., Semmak, F., Bruel, J.M.: bCMS requirements modelling using SysML/KAOS
Gnaho, C., Semmak, F., Laleau, R.: An overview of a SysML extension for goal-oriented NFR modelling. In: RCIS 2013, Paris, France, 29–31 May 2013, pp. 1–2. IEEE (2013)
Hause, M., et al.: The SysML modelling language. In: Fifteenth European Systems Engineering Conference, vol. 9. Citeseer (2006)
Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202–204. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04570-7_17
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, Chichester (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
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Mashkoor, A., Jacquot, J.: Utilizing Event-B for domain engineering: a critical analysis. Requir. Eng. 16(3), 191–207 (2011)
Mashkoor, A., Jacquot, J.: Validation of formal specifications through transformation and animation. Requir. Eng. 22(4), 433–451 (2017)
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 (2011)
Openflexo: Openflexo project (2019). http://www.openflexo.org
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 (2004). https://doi.org/10.1007/978-1-4020-8157-6_2
Sengupta, K., Hitzler, P.: Web ontology language (OWL). In: Staab, S., Studer, R. (eds.) Encyclopedia of Social Network Analysis and Mining, pp. 2374–2378. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-540-24750-0_4
Tueno, S., Frappier, M., Laleau, R., Mammar, A., Barradas, H.R.: The Generic SysML/KAOS Domain Metamodel. ArXiv e-prints, cs.SE, 1811.04732, November 2018
Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Towards using ontologies for domain modeling within the SysML/KAOS approach. In: IEEE Proceedings of MoDRE Workshop, 25th IEEE International Requirements Engineering Conference
Tueno, S., Laleau, R., Mammar, A., Frappier, M.: Formal representation of SysML/KAOS domain models. ArXiv e-prints, cs.SE, 1712.07406, December 2017
Van Lamsweerde, A.: Requirements Engineering: From System Goals to UML Models to Software, vol. 10. Wiley, Chichester (2009)
Yu, E.S.K.: Towards modeling and reasoning support for early-phase requirements engineering. In: RE, pp. 226–235. IEEE Computer Society (1997)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Tueno Fotso, S.J., Laleau, R., Frappier, M., Mammar, A., Thibodeau, F., Nsangou Mouchili, M. (2019). Assessment of a Formal Requirements Modeling Approach on a Transportation System. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_29
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_29
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)