Information Technology Reference
In-Depth Information
Applying Event-B Atomicity Decomposition to a
Multi Media Protocol
Asieh Salehi Fathabadi and Michael Butler
University of Southampton
asf08r,mjb@ecs.soton.ac.uk
Abstract.
Atomicity Decomposition is a technique in the Event-B for-
mal method, which augments Event-B refinement with additional struc-
turing in a diagrammatic notation to support complex refinement in
Event-B. This paper presents an evaluation of Event-B atomicity decom-
position technique in modeling a multi media case study with the dia-
grammatic notation. Firstly the existing technique and the diagrammatic
notation are shown. Secondly an evaluation is performed by developing
a model of a Media Channel System. A Media Channel is established
between two endpoints for transferring multi-media data. Finally some
extensions to the existing diagrammatic notation are proposed and ap-
plied to the multi-media case study.
Keywords:
Event-B, Refinement, Atomicity Decomposition, Structured
Event Refinement.
1
Introduction
Event-B [1, 2] is a formal method that uses the concept of refinement [3, 4] in
modeling. Event-B modeling starts with an abstraction of a system and adds
details during refinement levels in order to gain a final model close to the im-
plementation. Moreover mathematical proofs are incorporated into Event-B to
verify the correctness of refinement steps.
The most important benefit of using Event-B is its capability to use abstrac-
tion and refinement. In this approach the modeling process starts with an ab-
straction of the system which speifies the goals of the system. In our case study,
a media channel system, establishing and modifying the established channel are
the main system goals. The abstract level of our Event-B model shows these
goals in a very general way, and then during refinement levels, features of the
protocol are modeled and the goals are achieved in a detailed way. Moreover tool
support is another benefit of using Event-B. The Rodin tool [5] supports proof
obligation generation and automated proof. Through a refinement approach, we
prove that the abstract goals concerning establishment and modification of me-
dia channels are satisfied by the detailed protocol. In the developed Event-B
models of the media channel system reported here, all proofs are generated and
discharged by the Rodin tool.
