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

lat, long ← OPMerge =
VAR lat gps, long gps, lat wifi, long wifi, ponderation gps, ponderation wifi
IN lat gps := get lat(gps loc) ||
long gps := get long(gps loc) ||
ponderation gps := get pond(gps loc) ||
lat wifi := get lat(wifi loc) ||
long wifi := get long(wifi loc) ||
ponderation wifi := get pond(wifi loc) ;
lat := ((lat gps ∗ ponderation gps) + (lat wifi ∗ ponderation wifi))
/ (ponderation gps + ponderation wifi) ||
long := ((long gps ∗ ponderation gps) + (long wifi ∗ ponderation wifi))
/ (ponderation gps + ponderation wifi)
END
Fig. 7. The B operation OPMerge
4 Lessons Learned
The first conclusion that can be drawn from this experience concerns the va-
lidity of our approach. The elaboration of the specification of the localization
component has been carried out with specialists of the domain, with no skills in
formal and GORE methods. Four observations can be stated. Firstly, the visual
dimension (boxes, arrows...) can assist people to better understand requirements.
Secondly, GORE methods help designers to structure the Event-B specification
and to choose the relevant refinement level to introduce the different Event-B
events. Thirdly, these methods aid designers to correctly build guards of each
Event-B event. For instance, at the most abstract level, the guard of Local-
izeVehicle is set to TRUE to express that the event is always feasible. The
definitive guard is built during the refinement process. Finally, the employment
of GORE encourages designers to consider both the system and its environment.
In our view, explicitly expressing the notion of ordering, interleaving and
exclusivity between events is a useful addition to the Event-B refinement se-
mantics. Up to now, encoding these notions is possible in the current state of
Event-B using extra model variables (flags) embedded into guards and event
actions. The drawback of such extra model variables is the entanglement of or-
der encoding and functional specification. This entanglement makes traceability
between requirements and specification complicated. The proposed Event-B re-
finement extension (without extra model variables) makes such Event-B models
more readable and may allow a proof obligation economy. This last benefit is
under study and must be normally confirmed by further case studies.
5 Related Work
Most of the existing work aiming at establishing links between requirements mod-
els and formal methods consider KAOS and B or VDM++. The work of [13]