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

It is also important to indicate that the most important feature provided by
Event-B is its ability to stepwise refine specifications. Refinement is a process
that often transforms an abstract and non-deterministic specification into a con-
crete and deterministic system that preserves the functionality of the original
specification. During the refinement, event descriptions are rewritten to take
new variables into account. This is performed by strengthening their guards and
adding substitutions on the new variables. New events that only assign the new
variables may also be introduced. Notice that the state of the abstract machine
is related to the state of the concrete machine by a gluing invariant J ( v,w ),
where v are the variables of the abstract machine and w the variables of the con-
crete machine. In addition to the invariant preservation , other proof obligations
(POs) are generated to ensure the correctness of the refinement with respect
to the abstract machine: (i) the guard strengthening ensures that the concrete
guard is stronger than the abstract one. In other words, it is not possible to
have the concrete version enabled whereas the abstract one would not. The term
”stronger” means that the concrete guard implies the abstract guard. (ii) the
correct refinement ensures that the concrete event transforms the concrete vari-
ables in a way which does not contradict the abstract event. Event-B is provided
with tool support in the form of an Eclipse-based IDE called Rodin [7].
3 Experience with the Specification of a Localization
Software Component
A localization system is a critical part of a land transportation system. Many
positioning systems have been proposed over the last years. GPS, one of the
most widely used positioning system, is perhaps the best-known. This system
belongs to the GNSS (Global Navigation Satellite Systems) family which also
regroups GALILEO or GLONASS. Positioning systems are often dedicated to
a particular environment; the GNSS technology, for example, generally does
not work indoors. To resolve these problems, numerous alternatives relying on
very different technologies have arisen. These last years, Wireless LAN such
as IEEE 802.11 networks have been considered by numerous location systems.
These systems use the radio signal strength to determine the physical location.
Localization systems can therefore be designed using various technologies like
wireless personal networks such as Wifi or Bluetooth [17,18], GNSS repeaters or
visual landmarks.
When elaborating a goal model, the main diculties are first to identify goals
and then to specify links between these goals. Often, requirements engineers
need to search through preliminary documents in order to extract goals (key
properties) using a number of heuristics (asking HOW and WHY questions...)
detailed in [4]. Figure 1 shows the obtained KAOS goal model of a localization
component thanks to heuristics. For example, a HOW question about the goal
G would then lead to the goals G 1 , G 2 and G 3 . This KAOS goal model contains:
(i) high-level goals; (ii) refinement links denoted by a bubble linking the parent
goal with an arrow, and the child goals with regular lines; (iii) requirements