Applying Event-B Atomicity Decomposition to a Multi Media Protocol

Abstract. Atomicity Decomposition is a technique in the Event-B formal method, which augments Event-B refinement with additional structuring in a diagrammatic notation to support complex refinement in Event-B. This paper presents an evaluation of Event-B atomicity decomposition technique in modeling a multi media case study with the diagrammatic 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 applied to the multi-media case study. Key words: Event-B, Refinement, Atomicity Decomposition, Structured Event Refinement

• Type: Journal
• Year: 2009
• Where: FMCO
• Authors: Asieh Salehi Fathabadi, Michael Butler
• Keywords: Atomicity Decomposition, Atomicity Decomposition Technique, Diagrammatic Notation, FMCO 2009, Formal Methods