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

MACHINE Localization2
REFINES Localization1
SEES TypeSets
VARIABLES
gps loc , wifi loc , sensors loc , kept loc
INVARIANTS
inv1 : gps loc

LONGITUDE )
inv2 : wifi loc ∈{wifi}→ ( LATITUDE × LONGITUDE )
inv3 : subcomponents loc = gps loc ∪ wifi loc
inv4 : sensors loc ∈ SUBSENSORS

∈{ gps }→ ( LATITUDE ×

→ ( LATITUDE × LONGITUDE )

inv5 : kept loc ∈ SUBCOMPONENTS → ( LATITUDE × LONGITUDE )

inv6 : validated loc = kept loc
EVENTS
Initialisation
begi act6 : gps loc :

)
act7 : wifi loc : ∈{wifi}→ ( {null}×{null } )
act8 : sensors loc : ∈ SUBSENSORS → ( {null}×{null} )
act9 : kept loc : ∈ SUBCOMPONENTS → ( {null}×{null } )

∈{ gps }→ ( { null }×{ null }

end
Event UseGPS =
begi act1 : gps loc : ∈{gps}→ (( LATITUDE \{null } ) × ( LONGITUDE \{null } ))
end
Event UseWIFI =
begi act1 : wifi loc : ∈{wifi}→ (( LATITUDE \{null } ) × ( LONGITUDE \{null } ))
end
Event CaptureRelativeLocalizations =

whe grd1 : subcomponents loc

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

( LONGITUDE \{ null } ))

then act1 : sensors loc

| ( sensors loc : ∈ SUBSENSORS → (( LATITUDE \

{null } ) × ( LONGITUDE \{null } ))) ∧ sensors loc = ∅

end
Event FilterData =
whe grd1 : sensors loc

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

( LONGITUDE \{ null } )) ∧ sensors loc = ∅

then act1 : kept loc : ∈ P 1 ( subcomponents loc )
end
END

Fig. 5. Second Event-B refinement model

- One “correct refinement” PO is also proved since the conjunction of the two
concrete postconditions implies the abstract postcondition under the gluing
invariant inv 3. Hence, this ensures that subcomponents loc is a total func-
tion (see the postcondition of the abstract event CaptureRawLocalizations).