Assessment of a Formal Requirements Modeling Approach on a Transportation System

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.