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

MACHINE Localization3
REFINES Localization2
SEES TypeSets
VARIABLES
sensors loc , speed loc , accel loc
INVARIANTS
inv1 : speed loc

∈{ speed }→ ( LATITUDE × LONGITUDE )

LONGITUDE )
inv3 : ( sensors loc = speed loc ) ∨ ( sensors loc = accel loc ) ∨ ( sensors loc =
speedloc ∪ accel loc )
EVENTS
Initialisation
begi act10 : speed loc :

inv2 : accel loc

∈{ accel }→ ( LATITUDE ×

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

act11 : accel loc :

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

end
Event UseSpeedSensor =
refines CaptureRelativeLocalizations
whe grd1 : subcomponents loc

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

( LONGITUDE \{null } ))
grd2 : accel loc ∈{accel}→ ( {null}×{null } )
then act1 : speed loc

( speed loc ∈{

, sensors loc : | speed }→ (( LATITUDE \

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

end
Event UseAccelerometer =
refines CaptureRelativeLocalizations
whe grd1 : subcomponents loc

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

( LONGITUDE \{ null } ))

)
then act1 : accel loc, sensors loc : | ( accel loc ∈{accel}→ (( LATITUDE\{null} ) ×
( LONGITUDE \{null } ))) ∧ sensors loc = accel loc

grd2 : speed loc

∈{ speed }→ ( { null }×{ null }

end
END

Fig. 6. Third Event-B refinement model

proof obligations (“guard strengthening” and “correct refinement”) could be dis-
charged by the current version of the Rodin automatic theorem prover [7]. This
is due essentially to the gluing invariant inv3 and the individual guards of each
event. However, we require to express two additional proof obligations ensuring
that only one event (either UseSpeedSensor or UseAccelerometer ) but not
both can be executed. These two proof obligations are discharged since (i) the
postcondition of UseSpeedSensor forbids the guard of UseAccelerometer
to be triggered; (ii) the postcondition of UseAccelerometer forbids the guard
of UseSpeedSensor to be triggered.
This is the last step of refinement since all the goals are either requirements
or expectations (see Figure 1).