TY - GEN
T1 - On the use of domain and system knowledge modeling in goal-based Event-B specifications
AU - Mammar, Amel
AU - Laleau, Régine
N1 - Publisher Copyright:
© Springer International Publishing AG 2016.
PY - 2016/1/1
Y1 - 2016/1/1
N2 - When using formal methods, one of the main difficulties is to elaborate the initial formal specification from informal descriptions obtained during the requirements analysis phase. For that purpose, we propose a goal-based approach in which the building of an initial formal model (in Event-B) is driven by a goal-oriented requirements engineering model (SysML/KAOS). In a previous work, we have defined a set of rules to derive a partial Event-B specification from a goal model. In this paper, we propose to enhance the goal model in order to obtain a more complete formal specification. First, we advocate the specification of a domain ontology in order to share common understanding of the structure of the different applications of the underlying domain. This is particularly useful for complex systems to explicit and make clearer the domain knowledge. For a specific system, a class and an object diagrams are then specified to detail its components and their relationships. Finally, we describe how the ontology and the structural model are translated into Event-B. The proposed approach is illustrated through a landing gear system.
AB - When using formal methods, one of the main difficulties is to elaborate the initial formal specification from informal descriptions obtained during the requirements analysis phase. For that purpose, we propose a goal-based approach in which the building of an initial formal model (in Event-B) is driven by a goal-oriented requirements engineering model (SysML/KAOS). In a previous work, we have defined a set of rules to derive a partial Event-B specification from a goal model. In this paper, we propose to enhance the goal model in order to obtain a more complete formal specification. First, we advocate the specification of a domain ontology in order to share common understanding of the structure of the different applications of the underlying domain. This is particularly useful for complex systems to explicit and make clearer the domain knowledge. For a specific system, a class and an object diagrams are then specified to detail its components and their relationships. Finally, we describe how the ontology and the structural model are translated into Event-B. The proposed approach is illustrated through a landing gear system.
U2 - 10.1007/978-3-319-47166-2_23
DO - 10.1007/978-3-319-47166-2_23
M3 - Conference contribution
AN - SCOPUS:84993965317
SN - 9783319471655
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 325
EP - 339
BT - Leveraging Applications of Formal Methods, Verification and Validation
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Verlag
T2 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Y2 - 10 October 2016 through 14 October 2016
ER -