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

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on software engineering 2013-03, Vol.39 (3), p.361-383
Main Authors: Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.
Format: Article
Language:English
Subjects:
Adaptation models
Artificial intelligence
behavior model refinement
Calculus
Computational modeling
goal operationalization
inductive learning
Iterative methods
Learning
model checking
Objectives
Requirements
Requirements elaboration
Requirements specifications
Semantics
Software
Software engineering
Studies
Switches
Wheels
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0098-5589
1939-3520
DOI:10.1109/TSE.2012.41