Information Technology Reference
In-Depth Information
Modeling of large and complex systems can result in large and complex mod-
els and dicult proofs [6]. Refinement techniques can address this complexity.
In Event-B refinement, rather than having a single large model, it is common
to represent a desired outcome as an abstract atomic event and then decompose
that into smaller sub-events in subsequent refinement levels. If the abstraction
gaps between refinement levels are small, it means relatively small details are
added in each refinement level and proof obligations would be relatively easy to
discharge. Most of proof obligations are related to consistency between refine-
ment levels, so with the small gaps these proofs become easier to discharge. This
will be explained more in the next section when we introduce invariants.
Although refinement offers the advantages outlined above, the Event-B
refinement method does not explicitly represent all refinement connections be-
tween abstract and concrete events. Atomicity decomposition diagrams provide
a structuring technique which addresses this through a diagrammatic notation.
The atomicity decomposition technique helps to structure refinement in Event-B.
This technique is introduced in [7]. It is intended to make the standard refine-
ment rules clearer and their application more systematic. In Event-B refinement
there is no clear connection between certain actions of different refinement lev-
els. The diagrammatic notation of atomicity decomposition shows relationships
between refinement levels. In this approach usually a single event shows the goal
in the abstract level, and then it is decomposed to sub-events in refinement.
The contribution of this paper is applying existing Event-B atomicity decom-
position technique to a multi media case study. An evaluation of this technique
in modeling the multi media system is presented. There are several contributions
in this evaluation. First we will see how system goals are modeled in the abstract
level with single events. Then details of the protocol are added gradually dur-
ing refinement levels. For applying these details we will see how the atomicity
decomposition diagrammatic notation will help us to structure refinement in an
explicit way. Finally this development leads to discharge of all proof obligations
using the Rodin tool-set.
In this paper after a short background about Event-B, we will explore how the
diagrammatic notation for atomicity decomposition of [7] can help to structure
refinement in Sect. 3. Then an incremental development of an existing multi-
media protocol using this technique will be presented. In this protocol, a media
channel is a point-to-point and dynamic channel, established for transferring
multi-media data between two endpoints, called initiator and acceptor. In the
previous paper [7] the connection between the requirements of a system and
the decomposition technique was not explicitly discussed. In this paper we will
see how requirements of the system are linked with levels in the atomicity de-
composition diagram. The current atomicity decomposition technique provides
sucient patterns in development of media channel system in most of refinement
levels. However some extensions to the diagrammatic technique are proposed and
applied to the case study.
 
Search WWH ::




Custom Search