Deriving Non-zeno Behavior Models from Goal Models Using ILP
This paper addresses the problem of automated derivation of non-zeno behaviour models from goal models. The approach uses a novel combination of model checking and machine learning. We first translate a goal model formalised in linear temporal logic into
- PDF / 580,635 Bytes
- 15 Pages / 430 x 660 pts Page_size
- 103 Downloads / 206 Views
Imperial College London {da04,ar3,su2}@doc.ic.ac.uk 2 University of Buenos Aires [email protected]
Abstract. This paper addresses the problem of automated derivation of non-zeno behaviour models from goal models. The approach uses a novel combination of model checking and machine learning. We first translate a goal model formalised in linear temporal logic into a (potentially zeno) labelled transition system. We then iteratively identify zeno traces in the model and learn operational requirements in the form of preconditions that prevent the traces from occurring. Identification of zeno traces is acheived by model checking the behaviour model against a time progress property expressed in linear temporal logic, while learning operational requirements is achieved using Inductive Logic Programming. As a result of the iterative process, not only a non-zeno behaviour model is produced but also a set of preconditions that, in conjunction with the known goals, ensure the non-zeno behaviour of the system.
1
Introduction
Goal oriented requirements engineering (GORE) is an increasingly popular approach to elaborating software requirements. Goals are prescriptive statements of intent whose satisfaction requires the cooperation of components in the software and its environment. One of the limitations of approaches to GORE [5,6,14] is that the declarative nature of goals hinders the application of a number of successful validation techniques based on executable models such as graphical animations, simulations, and rapid-prototyping. They do not naturally support narrative style elicitation techniques, such as those in scenario-based requirements engineering and are not suitable for down-stream analyses that focus on design and implementation issues which are of an operational nature. To address these limitations, techniques have been developed for constructing behaviour models automatically from declarative descriptions in general [22] and goal models specifically [12]. The core of these techniques is based on temporal logic to automata transformations developed in the model checking community. For instance, in [12] Labelled Transition Systems (LTS) are built automatically from KAOS goals expressed in Fluent Linear Temporal Logic (FLTL) [8].
We acknowledge EPSRC EP/CS541133/1, ANPCyT PICT 11738, and the Levehulme Trust for partially funding this work.
J. Fiadeiro and P. Inverardi (Eds.): FASE 2008, LNCS 4961, pp. 1–15, 2008. c Springer-Verlag Berlin Heidelberg 2008
2
D. Alrajeh, A. Russo, and S. Uchitel
The key technical difficulty in constructing behaviour model from goal models is that the latter are typically expressed in a synchronous, non-interleaving semantic framework while the former have an asynchronous interleaving semantics. This mismatch relates to the fact that it is convenient to make different assumptions for modelling requirements and system goals than for modelling communicating sequential processes. One of the practical consequences of this mismatch is that the construction of behaviour models from a
Data Loading...
