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

CONTEXT TypeSets
SET SUBCOMPONENTS
SUBSENSORS
CONSTANTS
gps , wifi , LATITUDE , LONGITUDE
null , speed , accel
AXIOMS
axm1 : partition ( SUBCOMPONENTS , {gps}, {wifi} )
axm2 : LATITUDE =

N ∪{ null }

}
axm4 : partition ( SUBSENSORS , {speed}, {accel} )
END

axm3 : LONGITUDE = N ∪{ null

Fig. 3. The Event-B context TypeSets

Goal G 1 : Achieve [CaptureRawLocalizations]
InformalDef: Firstly, several sets of raw localization data are captured
by using different technologies.

Goal G 2 : Achieve [ValidateData]
InformalDef: Then, all the sets of raw localization data will be validated
and controlled.

Goal G 3 : Achieve [MergeData]
InformalDef: Finally, all the validated data will be merged in order to
obtain the final localization.

Similarly, we associate an Event-B refinement model Localization1 ,in
Figure 4, to this first level of the hierarchy of the KAOS goal graph. The sub-goals
G 1 , G 2 and G 3 are represented by three Event-B events CaptureRawLocal-
izations , ValidateData and MergeData , respectively. The first one returns
a set of couples (latitude, longitude), one for each component used for localizing
a vehicle. The second one validates the returned set of couples by choosing the
acceptable values. The final one returns the final localization calculated from the
returned values of the event MergeData .
In Event-B, often the information about such event ordering has to be embed-
ded into guards and event actions with the downside of extra model variables. For
that, we have chosen to explicitly reproduce KAOS goal ordering in an Event-B
model by proposing a syntactic extension of the Event-B refinement proof rule
in order to provide a way to refine an abstract event by a sequence of new events.
Hence, the abstract event LocalizeVehicle is refined as follows:

( CaptureRawLocalizations ; ValidateData ; MergeData ) Refines
LocalizeVehicle