Loose Observation in Event-B

Refinement of Event-B machines is based on changing internal variables to obtain different data representations. One approach is expressed only in terms of internal variables. In the extreme case it permits refining a machine by another by choosing the gluing invariant “true”. The other one is based on relating external variables that can be refined functionally, so that properties expressed in terms of external variables are preserved. In practice, the first approach is used and gluing invariants are suitably chosen to achieve a meaningful relationship between refined machines. The second approach is based on the idea of observing a machine in terms of its external variables. It is more complicated, restrictive and not commonly used. In this paper we propose a different approach to observing Event-B machines that is more constraining than the first approach but less complicated and restrictive than the second approach. We extend Event-B refinement by permitting introducing new events and eliminating old events. The concept of observation is made more flexible by permitting non-observation of certain states as well as observing sets of values related to a states. Although this complicates relating observed fixed points and traces of machines, the proof obligations remain uncomplicated.