TY - GEN
T1 - Formalising the requirements of an e-voting software product line using event-B
AU - Wakrime, Abderrahim Ait
AU - Gibson, J. Paul
AU - Raffy, Jean Luc
N1 - Publisher Copyright:
© 2018 IEEE.
PY - 2018/10/17
Y1 - 2018/10/17
N2 - A Software Product Line (SPL) is a tool/method used to generate a family of program/system variants for a specific domain, and to support a more efficient software development of future products within the same domain. A Feature Model (FM) is a popular graphical/textual representation used in SPL requirements specification; it is used to capture commonality and variability information existing in an SPL as a set of inter-related and configurable features. A concrete model of an SPL instance is obtained by binding the variation information in the FM with a configuration that meets a specific set of feature requirements. Since configuration decisions are taken prior to instantiation, invalid configurations should be detected/avoided before design begins. This paper addresses the problem of the verification of the correctness (validity) of FM instances and FM configuration during requirements modelling. It proposes a requirements model based on Event-B contexts, allowing us to check the correctness of a given configuration, before starting the correct-by-construction design and implementation process, based on refinement.
AB - A Software Product Line (SPL) is a tool/method used to generate a family of program/system variants for a specific domain, and to support a more efficient software development of future products within the same domain. A Feature Model (FM) is a popular graphical/textual representation used in SPL requirements specification; it is used to capture commonality and variability information existing in an SPL as a set of inter-related and configurable features. A concrete model of an SPL instance is obtained by binding the variation information in the FM with a configuration that meets a specific set of feature requirements. Since configuration decisions are taken prior to instantiation, invalid configurations should be detected/avoided before design begins. This paper addresses the problem of the verification of the correctness (validity) of FM instances and FM configuration during requirements modelling. It proposes a requirements model based on Event-B contexts, allowing us to check the correctness of a given configuration, before starting the correct-by-construction design and implementation process, based on refinement.
KW - E-Voting
KW - Event-B
KW - Feature Model Configuration
KW - Formal Modelling
KW - Software Product Lines
UR - https://www.scopus.com/pages/publications/85057323710
U2 - 10.1109/WETICE.2018.00022
DO - 10.1109/WETICE.2018.00022
M3 - Conference contribution
AN - SCOPUS:85057323710
T3 - Proceedings - 2018 IEEE 27th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2018
SP - 54
EP - 57
BT - Proceedings - 2018 IEEE 27th International Conference on Enabling Technologies
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 27th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2018
Y2 - 27 June 2018 through 29 June 2018
ER -