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

MACHINE Localization1
REFINES Localization
SEES TypeSets
VARIABLES
subcomponents loc , validated loc , merged loc
INVARIANTS
inv1 : subcomponents loc

∈ SUBCOMPONENTS → ( LATITUDE ×

LONGITUDE )
inv2 : validated loc ∈ SUBCOMPONENTS

→ ( LATITUDE × LONGITUDE )

LONGITUDE
inv4 : estimated loc = merged location
EVENTS
Initialisation
begi act2 : subcomponents loc :

inv3 : merged loc ∈ LATITUDE ×

∈ SUBCOMPONENTS → ( { null }×{ null } )

act3 : validated loc : ∈ SUBCOMPONENTS → ( {null}×{null} )
act4 : merged loc := null

→ null

end
Event CaptureRawLocalizations =
begi act1 : subcomponents loc :

∈ SUBCOMPONENTS → (( LATITUDE \{ null } ) ×

( LONGITUDE \{ null } ))

end
Event ValidateData =
whe grd1 : subcomponents loc

∈ SUBCOMPONENTS → (( LATITUDE \{ null } ) ×

( LONGITUDE \{null} ))
then act1 : validated loc :

∈ P 1 ( subcomponents loc )

end
Event MergeData =
whe grd1 : validated loc

∈ P 1 ( subcomponents loc )
grd2 : subcomponents loc ∈ SUBCOMPONENTS → (( LATITUDE \{ null } ) ×

( LONGITUDE \{null} ))
then act1 : merged loc :

∈ ( LATITUDE \{ null } ) × ( LONGITUDE \{ null } )

end

Fig. 4. First Event-B refinement model

In addition to the feasibility proof obligation 2 , this kind of refinement requires
to discharge these different proof obligations:

- Two ordering constraints express the “milestone” characteristic between the
Event-B events. These two proof obligations are discharged: (i) the action of
CaptureRawLocalizations implies the guard of ValidateData (ii) the
action of ValidateData implies the guard of MergeData .
- One “guard strengthening” PO is also discharged since the first event in the
sequence ( CaptureRawLocalizations )hasaguard( true )thatimpliesthe
abstract guard ( true ).

2 It ensures that each event must also be feasible, in a sense that an appropriate new
state v must exist for some given current state v under the invariant I(v).