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

Second Refinement: Applying the Milestone Goal Refinement Pattern
On the other hand, the goal G 2 is refined into two sub-goals according to the
milestone goal refinement pattern (the order is from left to right):
Goal 2 . 1 : Achieve [CaptureRelativeLocalizations]
InformalDef: At first, several sets of relative localization data are cap-
tured by using different technologies.
Goal 2 . 2 : Achieve [FilterData]
InformalDef: Then, all the sets of raw localization data will be filtered.
All these subgoals are translated into new events using the same rules as for
LocalizeVehicle in the abstract Event-B model. As for the first refinement, the
abstract event ValidateData is refined by the sequence of all the new events
( CaptureRelativeLocalizations , FilterData ) as follows:
( CaptureRelativeLocalizations ; FilterData ) Refines ValidateData
We have also discharged the different proof obligations related to the milestone
refinement such as the ordering constraint , the “guard strengthening” and the
“correct refinement” .
3.4 Third Refinement
The goal G 2 . 1 is OR-refined in two subgoals:
Goal G 2 . 1 . 1 : Achieve [UseSpeedSensor]
InformalDef: The Vehicle may use a speed sensor system.
Goal G 2 . 1 . 2 : Achieve [UseAccelerometer]
InformalDef: Or, it may use the accelerometer system.
Similarly, a refinement Event-B model Localization3 , in Figure 6, is associated
to this third level of the hierarchy of the goal graph. All these subgoals are
transformed into new Event-B events ( UseSpeedSensor , UseAccelerometer )
by using the same transcription rules as for the event LocalizeVehicle in the
abstract Event-B model. Since the satisfaction of exactly one KAOS sub-goal
implies the satisfaction of the parent goal, we propose to refine the abstract
event CaptureRelativeLocalizations as follows:
( UseSpeedSensor XOR UseAccelerometer ) Refines
CaptureRelativeLocalizations
This Event-B refinement semantics is quite close to the same one proposed by
Rodin [7] if we consider that each event refines the abstract event. Hence, the