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

3.5 Synthesis
Regarding the proof activity linked to the use of Event-B, in addition to the clas-
sical proof obligations such as feasibility proof obligations, the resulting Event-B
specification led to a number of 16 additional custom-built proof obligations (rel-
atively simple) that have been proved totally. Most of these proof obligations
can be automatically discharged by the Rodin tool.
Unfortunately, discharging the different proof obligations is not su cient in
order to validate the conformance of the specification to original requirements. In
fact, we can never ensure that the expression of the Event-B event corresponds
exactly to the expression of the related goal since this latter is informal. For that,
we can use an animation technique to validate the derived formal specification
against original customers' requirements. This animation step not only indicates
deviations from original requirements right on the spot but also helps fixing
some specification errors. The reader can refer to [16] for more details. For that,
ProB [14] may be a very useful validation tool since its automated animation
facilities allow users to animate their specifications; i.e. gain confidence in their
specifications.
The obtained abstract Event-B model is then further refined towards an im-
plementation. It concerns only the Event-B events corresponding to require-
ments assigned to software agents. Otherwise, an expectation (assigned to an
external agent) is a property required on the environment and its corresponding
Event-B event will not be implemented in the software-to-be. More precisely,
in our case study, the Event-B events UseGPS , UseWIFI , UseSpeedSensor
and UseAccelerometer are not refined since they correspond to goals of type
expectation . They are implemented by hardware components (GPS, WIFI com-
ponents...) in a vehicle. Only the Event-B events FilterData and MergeData
are further refined. For example, the refinement of the Event-B event Merge-
Data leads to a software that implements the algorithm chosen to realize the
fusion (thanks to the B operation OPMerge ) as shown in Figure 7. At first,
this operation recovers all the raw localization data from both GPS and WIFI
thanks to the call of operations get lat and get long . Then, the call of the op-
eration get pond serves to verify if the returned values of GPS and WIFI are
validated or no. If these values are validated, then get pond returns a weighting
value set to 1 (0 otherwise). Finally, the operation calculates the final latitude
and longitude based on the different weighting values.
An interesting result is that the link between the B operation OPMerge and
the abstract Event-B event MergeData (see Figure 4) can be ensured. While
the abstract event MergeData describes the properties that the final program
must fulfill, the B operation OPMerge describes the algorithm contained in
the program. Hence, MergeData describes the way by which we can eventually
judge that the final program OPMerge is correct: (i) the call of the operations
get lat and get long ensures the second guard of MergeData ;(ii)thecallofthe
operation get pond ensures the first guard of MergeData ; (iii) the final result of
the operation OPMerge (lat, long) satisfies the post-condition of MergeData .