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

- One “correct refinement” PO is also proved since the last event in the se-
quence ( MergeData ) has a postcondition that implies the abstract post-
condition under the gluing invariant inv 4. The sequence of concrete events
transforms the concrete variables in a way which does not contradict the
abstract event.

3.3 Second Refinement

Now, we consider the second level of the hierarchy of the KAOS goal graph. In the
same way, a refinement Event-B model Localization2 , in Figure 5, is created and
must refine the previous model Localization1 . This second refinement Event-B
model will encapsulate two KAOS refinement patterns:

Second Refinement: Applying the AND Goal Refinement Pattern. The
goal G 1 is AND-refined into two sub-goals; i.e. the conjunction of the sub-goals
is sucient to establish the satisfaction of the parent goal. This refinement spec-
ifies the kind of technology used to obtain localization data.

Goal G 1 . 1 : Achieve [UseGPS]
InformalDef: A GPS system is used.

Goal G 1 . 2 : Achieve [UseWIFI]
InformalDef: A wireless technique is used.

The sub-goals G 1 . 1 and G 1 . 2 are represented by two Event-B events UseGPS
and UseWIFI by using the same transcription rules as for the event Local-
izeVehicle in the abstract model. Since the goal G 1 is refined into two sub-goals
G 1 . 1 and G 1 . 2 according to the AND goal refinement pattern, the execution of
the corresponding new events must not necessary follows a specific order. For
that, our idea (inspired from Process Algebra [20]) is that these events ( UseGPS
and UseWIFI are executed in an arbitrary order: either UseGPS;UseWIFI
or UseWIFI;UseGPS . This corresponds to the semantics of the interleave op-
erator in process algebra. Of course, we must ensure that this AND refinement
manipulate only disjoint set of variables . Hence, we have proposed syntactic ex-
tension of the Event-B refinement proof rule in order to refine an abstract event
by the interleaving of all the new events as follows:

( UseGPS ||| UseWIFI ) Refines CaptureRawLocalizations

In addition to the feasibility proof obligation , the following proof obligations
must be discharged in order to prove such refinement:

- Two “guard strengthening” POs are discharged since the concrete guard of
the interleaved events ( UseGPS UseWIFI ) implies the abstract guard

( true )of CaptureRawLocalizations . In fact, the concrete guard is always
true (if we execute UseGPS at first or if we execute UseWIFI at first).

|||