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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Butler, M.: Incremental Design of Distributed Systems with Event-B. In: Marktoberdorf Summer School 2008 Lecture Notes. IoS (November 2008)
de Willem Roever, P., Engelhardt, K.: Data Refinement: Model-oriented Proof Theories and their Comparison Cambridge Tracts in Theoretical Computer Science, vol. 46. Cambridge University Press, Cambridge (1998)
Rezazadeh, A., Butler, M., Evans, N.: Redevelopment of an Industrial Case Study Using Event-B and Rodin. In: BCS-FACS Christmas 2007 Meeting - Formal Method. In: Industry (2007)
Abrial, J.-R., Butler, M., Hallerstede, S.: Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer, STTT (2010)
Abrial, J.-R.: Refinement, Decomposition and Instantiation of Discrete Models. In: Abstract State Machines, pp. 17–40 (2005)
Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, Springer, Heidelberg (2009)
Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)
Back, R.-J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)
Hallerstede, S.: Justifications for the Event-B Modelling Notation. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 49–63. Springer, Heidelberg (2006)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Zave, P., Cheung, E.: Compositional Control of IP Media. IEEE Trans. Software Eng. 35(1), 46–66 (2009)
Jackson, M.A.: System Development. Prentice-Hall, Englewood Cliffs (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salehi Fathabadi, A., Butler, M. (2010). Applying Event-B Atomicity Decomposition to a Multi Media Protocol. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds) Formal Methods for Components and Objects. FMCO 2009. Lecture Notes in Computer Science, vol 6286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17071-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-17071-3_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17070-6
Online ISBN: 978-3-642-17071-3
eBook Packages: Computer ScienceComputer Science (R0)