Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned - Formal Methods: Foundations and Applications - page 181

Fig. 1. KAOS goal model of a localization component
and their software responsibility agents; (iv) expectations and their environment
responsibility agents (GPS, WIFI, sensor and accelerometer).
Each goal is described informally in natural language. As we deal with func-
tional goals, we consider only Achieve goals of KAOS. An Achieve goal prescribes
intended behaviors where some target condition must sooner or later hold when-
ever some other condition holds in the current system state. An Achieve goal in
KAOS is denoted as follows where CurrentCondition is optional (said other-
wise, it can be true):
[if CurrentCondition then] sooner-or-later TargetCondition .
The approach we propose [10] starts from a KAOS goal model describing the
functional requirements of a system and derives an abstract Event-B specifica-
tion. The crux of our transformation is to express each KAOS functional goal
as an Event-B event, where: (i) the current condition of this goal is considered
as the guard; (ii) the then part encapsulates the target condition of this goal.
Afterwards, we have transformed into Event-B the different KAOS goal refine-
ment patterns (milestone, AND, OR) used to generate a KAOS goal hierarchy.
The main idea is that each level in the hierarchy of the KAOS goal graph is
represented as an Event-B model that refines the Event-B model related to the
previous level of the hierarchy. Then, we have proposed an Event-B transfor-
mation rule for each KAOS refinement pattern associated to functional goals
and we have identified for each one the systematic proof obligations. A formal
argumentation of the different identified proof obligations is detailed in [10].
In the next sections, we will use these different Event-B refinement relations
and additional custom-built proof obligations in order to transform the different
refinement levels of the goal model.