Elaborating requirements using model checking and inductive learning
The process of Requirements Engineering (RE) includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_00985589_v39_n3_p361_Alrajeh |
| Aporte de: |
| id |
todo:paper_00985589_v39_n3_p361_Alrajeh |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_00985589_v39_n3_p361_Alrajeh2023-10-03T14:56:58Z Elaborating requirements using model checking and inductive learning Alrajeh, D. Kramer, J. Russo, A. Uchitel, S. behavior model refinement goal operationalization inductive learning model checking Requirements elaboration Behavior model goal operationalization Inductive learning Operational requirements Positive examples Requirements elaboration Requirements specifications Iterative methods Model checking Specifications Learning systems The process of Requirements Engineering (RE) includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating a set of operational requirements that are complete with respect to given goals. We show how the integration of model checking and inductive learning can be effectively used to do this. The model checking formally verifies the satisfaction of the goals and produces counterexamples when incompleteness in the operational requirements is detected. The inductive learning process then computes operational requirements from the counterexamples and user-provided positive examples. These learned operational requirements are guaranteed to eliminate the counterexamples and be consistent with the goals. This process is performed iteratively until no goal violation is detected. The proposed framework is a rigorous, tool-supported requirements elaboration technique which is formally guided by the engineer's knowledge of the domain and the envisioned system. © 1976-2012 IEEE. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00985589_v39_n3_p361_Alrajeh |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
behavior model refinement goal operationalization inductive learning model checking Requirements elaboration Behavior model goal operationalization Inductive learning Operational requirements Positive examples Requirements elaboration Requirements specifications Iterative methods Model checking Specifications Learning systems |
| spellingShingle |
behavior model refinement goal operationalization inductive learning model checking Requirements elaboration Behavior model goal operationalization Inductive learning Operational requirements Positive examples Requirements elaboration Requirements specifications Iterative methods Model checking Specifications Learning systems Alrajeh, D. Kramer, J. Russo, A. Uchitel, S. Elaborating requirements using model checking and inductive learning |
| topic_facet |
behavior model refinement goal operationalization inductive learning model checking Requirements elaboration Behavior model goal operationalization Inductive learning Operational requirements Positive examples Requirements elaboration Requirements specifications Iterative methods Model checking Specifications Learning systems |
| description |
The process of Requirements Engineering (RE) includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating a set of operational requirements that are complete with respect to given goals. We show how the integration of model checking and inductive learning can be effectively used to do this. The model checking formally verifies the satisfaction of the goals and produces counterexamples when incompleteness in the operational requirements is detected. The inductive learning process then computes operational requirements from the counterexamples and user-provided positive examples. These learned operational requirements are guaranteed to eliminate the counterexamples and be consistent with the goals. This process is performed iteratively until no goal violation is detected. The proposed framework is a rigorous, tool-supported requirements elaboration technique which is formally guided by the engineer's knowledge of the domain and the envisioned system. © 1976-2012 IEEE. |
| format |
JOUR |
| author |
Alrajeh, D. Kramer, J. Russo, A. Uchitel, S. |
| author_facet |
Alrajeh, D. Kramer, J. Russo, A. Uchitel, S. |
| author_sort |
Alrajeh, D. |
| title |
Elaborating requirements using model checking and inductive learning |
| title_short |
Elaborating requirements using model checking and inductive learning |
| title_full |
Elaborating requirements using model checking and inductive learning |
| title_fullStr |
Elaborating requirements using model checking and inductive learning |
| title_full_unstemmed |
Elaborating requirements using model checking and inductive learning |
| title_sort |
elaborating requirements using model checking and inductive learning |
| url |
http://hdl.handle.net/20.500.12110/paper_00985589_v39_n3_p361_Alrajeh |
| work_keys_str_mv |
AT alrajehd elaboratingrequirementsusingmodelcheckingandinductivelearning AT kramerj elaboratingrequirementsusingmodelcheckingandinductivelearning AT russoa elaboratingrequirementsusingmodelcheckingandinductivelearning AT uchitels elaboratingrequirementsusingmodelcheckingandinductivelearning |
| _version_ |
1807318530281963520 |