Assessment of a Formal Requirements Modeling Approach on a Transportation System

Steve Jeffrey Tueno Fotso; Régine Laleau; Marc Frappier; Amel Mammar; Francois Thibodeau; Mama Nsangou Mouchili

doi:10.1007/978-3-030-32409-4_29

Assessment of a Formal Requirements Modeling Approach on a Transportation System

Steve Jeffrey Tueno Fotso
, Régine Laleau
, Marc Frappier
, Amel Mammar
, Francois Thibodeau
, Mama Nsangou Mouchili

Université de PARIS XII
Université de Sherbrooke
Ville de Montréal

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings
Editors	Yamine Ait-Ameur, Shengchao Qin
Publisher	Springer
Pages	470-486
Number of pages	17
ISBN (Print)	9783030324087
DOIs	https://doi.org/10.1007/978-3-030-32409-4_29
Publication status	Published - 1 Jan 2019
Event	21st International Conference on Formal Engineering Methods, ICFEM 2019 - Shenzhen, China Duration: 5 Nov 2019 → 9 Nov 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11852 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st International Conference on Formal Engineering Methods, ICFEM 2019
Country/Territory	China
City	Shenzhen
Period	5/11/19 → 9/11/19

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 11 Sustainable Cities and Communities

Keywords

B System
Domain modeling
Event-B
Formal models
Requirements engineering
Road transportation system
SysML/KAOS

Access to Document

10.1007/978-3-030-32409-4_29

Cite this

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 Y. Ait-Ameur, & S. Qin (Eds.), Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings (pp. 470-486). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11852 LNCS). Springer. https://doi.org/10.1007/978-3-030-32409-4_29

Tueno Fotso, Steve Jeffrey ; Laleau, Régine ; Frappier, Marc et al. / Assessment of a Formal Requirements Modeling Approach on a Transportation System. Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. editor / Yamine Ait-Ameur ; Shengchao Qin. Springer, 2019. pp. 470-486 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{c3c3a8722a2b48e5a74fdf2953f2dd5e,

title = "Assessment of a Formal Requirements Modeling Approach on a Transportation System",

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.",

keywords = "B System, Domain modeling, Event-B, Formal models, Requirements engineering, Road transportation system, SysML/KAOS",

author = "\{Tueno Fotso\}, \{Steve Jeffrey\} and R{\'e}gine Laleau and Marc Frappier and Amel Mammar and Francois Thibodeau and \{Nsangou Mouchili\}, Mama",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 21st International Conference on Formal Engineering Methods, ICFEM 2019 ; Conference date: 05-11-2019 Through 09-11-2019",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-32409-4\_29",

language = "English",

isbn = "9783030324087",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "470--486",

editor = "Yamine Ait-Ameur and Shengchao Qin",

booktitle = "Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings",

}

Tueno Fotso, SJ, Laleau, R, Frappier, M, Mammar, A, Thibodeau, F & Nsangou Mouchili, M 2019, Assessment of a Formal Requirements Modeling Approach on a Transportation System. in Y Ait-Ameur & S Qin (eds), Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11852 LNCS, Springer, pp. 470-486, 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, 5/11/19. https://doi.org/10.1007/978-3-030-32409-4_29

Assessment of a Formal Requirements Modeling Approach on a Transportation System. / Tueno Fotso, Steve Jeffrey; Laleau, Régine; Frappier, Marc et al.
Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. ed. / Yamine Ait-Ameur; Shengchao Qin. Springer, 2019. p. 470-486 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11852 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Assessment of a Formal Requirements Modeling Approach on a Transportation System

AU - Tueno Fotso, Steve Jeffrey

AU - Laleau, Régine

AU - Frappier, Marc

AU - Mammar, Amel

AU - Thibodeau, Francois

AU - Nsangou Mouchili, Mama

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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.

AB - 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.

KW - B System

KW - Domain modeling

KW - Event-B

KW - Formal models

KW - Requirements engineering

KW - Road transportation system

KW - SysML/KAOS

U2 - 10.1007/978-3-030-32409-4_29

DO - 10.1007/978-3-030-32409-4_29

M3 - Conference contribution

AN - SCOPUS:85076145310

SN - 9783030324087

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 470

EP - 486

BT - Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings

A2 - Ait-Ameur, Yamine

A2 - Qin, Shengchao

PB - Springer

T2 - 21st International Conference on Formal Engineering Methods, ICFEM 2019

Y2 - 5 November 2019 through 9 November 2019

ER -

Tueno Fotso SJ, Laleau R, Frappier M, Mammar A, Thibodeau F, Nsangou Mouchili M. Assessment of a Formal Requirements Modeling Approach on a Transportation System. In Ait-Ameur Y, Qin S, editors, Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. Springer. 2019. p. 470-486. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-32409-4_29

Assessment of a Formal Requirements Modeling Approach on a Transportation System

Abstract

Publication series

Conference

UN SDGs

Keywords

Access to Document

Fingerprint

Cite this