caa a22 4500 605516189 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150501xx s 000 0 eng 10.1007/s00165-014-0311-1 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0311-1 Language and tool support for event refinement structures in Event-B [Elektronische Daten] [Asieh Salehi Fathabadi, Michael Butler, Abdolbaghi Rezazadeh] 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. British Computer Society, 2014 Event refinement structure nationallicence Atomicity decomposition nationallicence Event-B nationallicence Formal method nationallicence Control flow nationallicence Refinement nationallicence Salehi Fathabadi Asieh Electronics and Software Systems Group, School of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK aut Butler Michael Electronics and Software Systems Group, School of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK aut Rezazadeh Abdolbaghi Electronics and Software Systems Group, School of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK aut Formal Aspects of Computing Springer London 27/3(2015-05-01), 499-523 0934-5043 27:3<499 2015 27 165 https://doi.org/10.1007/s00165-014-0311-1 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0311-1 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Salehi Fathabadi Asieh Electronics and Software Systems Group, School of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK aut NATIONALLICENCE 700 1- Butler Michael Electronics and Software Systems Group, School of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK aut NATIONALLICENCE 700 1- Rezazadeh Abdolbaghi Electronics and Software Systems Group, School of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/3(2015-05-01), 499-523 0934-5043 27:3<499 2015 27 165