Information Technology Reference
In-Depth Information
3.1 Abstract Model
Let us start by the high-level goal
G
which is defined as follows:
Goal
G
: Achieve [LocalizeVehicle]
InformalDef:
The vehicle must be localized.
We associate an Event-B model
Localization
, in Figure 2, to this most ab-
stract level of the hierarchy of the KAOS goal graph. In this Event-B model,
we will have an event called
LocalizeVehicle
that will translate the goal
G
;
i.e. it describes the “property” of the goal
G
, in terms of generalized substitu-
tions. Localizing a vehicle consists in obtaining an
estimated loc
which is a pair
of latitude and longitude. At this level of abstraction, it is not necessary to pre-
cise the way this information is calculated. Thus, we use the non-deterministic
generalized substitution through the symbol :
which specifies an unbounded
choice. So,
estimated loc
cantakeanyvalueinthesets(
LATITUDE\{null}
∈
)
and (
LONGITUDE \{null}
). The
null
value serves just to initialize the sys-
tem through the
initialization
event
1
. Notice that at this abstraction level, the
event
LocalizeVehicle
can always occur. Hence, its guard is always
true
.Sets
in uppercase are abstract sets used to type the variables. They are described in
the Event-B context
TypeSet s
(see in Figure 3).
MACHINE
Localization
SEES
TypeSets
VARIABLES
estimated loc
INVARIANTS
inv1
:
estimated loc
∈
LATITUDE
×
LONGITUDE
EVENTS
Initialisation
begi
act1
:
estimated loc
:=
null
→ null
end
Event
LocalizeVehicle
=
begi
act1
:
estimated loc
:
∈
(
LATITUDE \{null}
)
×
(
LONGITUDE \{null }
)
end
END
Fig. 2.
The abstract model
3.2 First Refinement
The goal
G
is refined into three sub-goals according to the milestone goal refine-
ment pattern (identifying milestone states from left to right):
1
Up to now, the initialization part, variables, invariants and contexts are manually
completed by the designer. It would be possible to derive them from domain models
in KAOS.
Search WWH ::
Custom Search