Abstract
Event-B is a formal method for modelling and verifying the consistency of chains of model refinements. The event refinement structure (ERS) approach augments Event-B with a graphical notation which is capable of explicit representation of control flows and refinement relationships. In previous work, the ERS approach has been evaluated manually in the development of two large case studies, a multimedia protocol and a spacecraft sub-system. The evaluation results helped us to extend the ERS constructors, to develop a systematic definition of ERS, and to develop a tool supporting ERS. We propose the ERS language which systematically defines the semantics of the ERS graphical notation including the constructors. The ERS tool supports automatic construction of the Event-B models in terms of control flows and refinement relationships. In this paper we outline the systematic definition of ERS including the presentation of constructors, the tool that supports it and evaluate the contribution that ERS and its tool make. Also we present how the systematic definition of ERS and the corresponding tool can ensure a consistent encoding of the ERS diagrams in the Event-B models.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial JR, Butler M, Hallerstede S, Son Hoang T, Mehta F, Voisin L: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12, 447–466 (2010)
Abrial JR: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (1996)
Abrial JR (2005) Refinement, decomposition and instantiation of discrete models. In: Proceedings of the 12th international workshop on abstract state machines, pp 17–40
Abrial JR: Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge (2010)
Back RJ, Kurki-Suonio R (1988) Distributed cooperation with action systems. ACM Trans Program Lang Syst, vol 10, pp 513–554
Butler M (2000) csp2B: a practical approach to combining CSP and B. Form Asp Comput 12:182–196. ISSN 0934-5043
Butler J (2009) Decomposition structures for Event-B. In: IFM2009. LNCS, vol 5423. Springer, Berlin
Crocker D, Overell P (2008) Augmented BNF for syntax specifications: ABNF. STD 68, RFC 5234
Eclipse [Online] (2013). http://www.eclipse.org
ESA Media Center, Space Science (2008) Factsheet: Bepicolombo. http://www.esa.int/esaSC
Hoare CAR (1985) Communicating sequential processes. Prentice Hall, Englewood Cliffs. ISBN 0-13-153289-8
Iliasov A (2009) On Event-B and control flow. Technical Report, School of Computing Science, Newcastle University, http://deploy-eprints.ecs.soton.ac.uk/144
Iliasov A (2010) Tutorial on the flow plugin for Event-B. Workshop on B Dissemination [WOBD] Satellite event of SBMF, Natal, Brazil
Jackson MA (1983) System development. Prentice-Hall, Englewood Cliffs
Kolovos D, Rose L, Paige R (2008) The epsilon book. http://www.eclipse.org/gmt/epsilon/doc/book
Metayer C, Abrial JR, Voisin L (2005) Event-B language. RODIN Project Deliverable 3.2. http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf
ProB Animator and Model Checker [Online] (2013). http://wiki.event-b.org/index.php/ProB
Salehi Fathabadi A, Butler M (2010) Applying Event-B atomicity decomposition to a multi media protocol. In: FMCO formal methods for components and objects, pp 89–104
Steinberg D, Budinsky F, Paternostro M, Merks E (2008) EMF: eclipse modeling framework, 2nd edn. Part of the eclipse series. Addison-Wesley Professional, Reading
Salehi Fathabadi A, Butler M, Rezazadeh R (2012) An approach to atomicity decomposition in the Event-B formal method. In: SEFM software engineering and formal methods, pp 78–93
Said MY, Butler M, Snook C (2008) UML-B and Event-B: an integration of languages and tools. In: The IASTED international conference on software engineering, pp 336–341
Said MY, Butler M, Snook C (2009) Language and tool support for class and state machine refinement in UML-B. In: FM2009-16th international symposium on formal methods, pp 579–595
Schneider S, Treharne H (2004) Verifying controlled components. In: Proc IFM, Springer, Berlin, pp 87–107
Salehi Fathabadi A, Rezazadeh A, Butler M (2011) Applying atomicity and model decomposition to a space craft system in Event-B. In: NASA formal methods, pp 328–342
Schneider S, Treharne H, Wehrheim H (2010) A CSP approach to control in Event-B. In: Proceedings of the 8th international conference on integrated formal methods, pp 260–274
Woodcock J, Davies J (1996) Using Z: specification, refinement and proof. Prentice hall international series in computer science. ISBN 0-13-948472-8
Woodcock J, Cavalcanti A (2002) The semantics of circus. In: ZB 2002: Formal specification and development in Z and B, 2nd international conference of B and Z users, pp 184–203
Zave P, Cheung E: Compositional control of IP media. IEEE Trans Softw Eng 35(1), 46–66 (2009)
Author information
Authors and Affiliations
Corresponding author
Additional information
George Eleftherakis and Jim Woodcock
Rights and permissions
About this article
Cite this article
Salehi Fathabadi, A., Butler, M. & Rezazadeh, A. Language and tool support for event refinement structures in Event-B. Form Asp Comp 27, 499–523 (2015). https://doi.org/10.1007/s00165-014-0311-1
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-014-0311-1