Decomposition Structures for Event-B Export

@incollection{citeulike:4257756, abstract = {Event-B provides a flexible approach to modelling and refinement of systems. In this paper we outline two important ways in which Event-B refinement can be augmented with additional structuring to support further the management of complex refinements. Firstly we show how event refinement diagrams can be used to structure refinement steps involving decomposition of atomicity. Secondly we outline a technique for decomposing models into sub-models to allow for independent refinement. We show how these two structuring techniques can be used together.}, author = {Butler, Michael}, citeulike-article-id = {4257756}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-00255-7_2}, citeulike-linkout-1 = {http://www.springerlink.com/content/3202127567642301}, doi = {10.1007/978-3-642-00255-7_2}, journal = {Integrated Formal Methods}, keywords = {event-scheduling, formalism}, pages = {20--38}, posted-at = {2009-09-06 08:38:55}, priority = {2}, title = {Decomposition Structures for Event-B}, url = {http://dx.doi.org/10.1007/978-3-642-00255-7_2}, year = {2009} }

TY - CHAP ID - citeulike:4257756 L3 - citeulike-article-id:4257756 N2 - Event-B provides a flexible approach to modelling and refinement of systems. In this paper we outline two important ways in which Event-B refinement can be augmented with additional structuring to support further the management of complex refinements. Firstly we show how event refinement diagrams can be used to structure refinement steps involving decomposition of atomicity. Secondly we outline a technique for decomposing models into sub-models to allow for independent refinement. We show how these two structuring techniques can be used together. JF - Integrated Formal Methods EP - 38 TI - Decomposition Structures for Event-B SP - 20 KW - event-scheduling KW - formalism AU - Butler, Michael PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-00255-7_2 ER -