TY - GEN
T1 - A formal requirements modeling approach
T2 - 14th International Conference on Software Technologies, ICSOFT 2019
AU - Fotso, Steve J.Tueno
AU - Laleau, Régine
AU - Barradas, Hector Ruiz
AU - Frappier, Marc
AU - Mammar, Amel
N1 - Publisher Copyright:
Copyright © 2019 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved.
PY - 2019/1/1
Y1 - 2019/1/1
N2 - This paper is about the formal specification of requirements of a rail communication protocol called Saturn, proposed by ClearSy systems engineering, a French company specialised in safety critical systems. The protocol was developed and implemented within a rail product, widely used, without modeling, verifying and even documenting its requirements. This paper outlines the formal specification, verification and validation of Saturn's requirements in order to guarantee its correct behavior and to allow the definition of slightly different product lines. The specification is performed according to SysML/KAOS, a formal requirements engineering method developed in the ANR FORMOSE project for critical and complex systems. System requirements, captured with a goal modeling language, give rise to the behavioral part of a B System specification. In addition, an ontology modeling language allows the specification of domain entities and properties. The domain models thus obtained are used to derive the structural part of the B System specification obtained from system requirements. The B System model, once completed with the body of events, can then be verified and validated using the whole range of tools that support the B method. Five refinement levels of the rail communication protocol were constructed. The method has proven useful. However, several missing features were identified. This paper also provides a formally defined extension of the modeling languages to fill the shortcomings.
AB - This paper is about the formal specification of requirements of a rail communication protocol called Saturn, proposed by ClearSy systems engineering, a French company specialised in safety critical systems. The protocol was developed and implemented within a rail product, widely used, without modeling, verifying and even documenting its requirements. This paper outlines the formal specification, verification and validation of Saturn's requirements in order to guarantee its correct behavior and to allow the definition of slightly different product lines. The specification is performed according to SysML/KAOS, a formal requirements engineering method developed in the ANR FORMOSE project for critical and complex systems. System requirements, captured with a goal modeling language, give rise to the behavioral part of a B System specification. In addition, an ontology modeling language allows the specification of domain entities and properties. The domain models thus obtained are used to derive the structural part of the B System specification obtained from system requirements. The B System model, once completed with the body of events, can then be verified and validated using the whole range of tools that support the B method. Five refinement levels of the rail communication protocol were constructed. The method has proven useful. However, several missing features were identified. This paper also provides a formally defined extension of the modeling languages to fill the shortcomings.
KW - B system
KW - Domain modeling
KW - Event-B
KW - Formal models
KW - Railway
KW - Requirements engineering
KW - Saturn rail communication protocol
KW - SysML/KAOS
U2 - 10.5220/0007809701700177
DO - 10.5220/0007809701700177
M3 - Conference contribution
AN - SCOPUS:85073118509
T3 - ICSOFT 2019 - Proceedings of the 14th International Conference on Software Technologies
SP - 170
EP - 177
BT - ICSOFT 2019 - Proceedings of the 14th International Conference on Software Technologies
A2 - van Sinderen, Marten
A2 - Maciaszek, Leszek
A2 - Maciaszek, Leszek
PB - SciTePress
Y2 - 26 July 2019 through 28 July 2019
ER -