Shared Event Composition/Decomposition in Event-B
Shared Event Composition/Decomposition in Event-B
复制标题
DOI：
10.1007/978-3-642-25271-6_7
复制
发表时间：
2010-11
期刊：
影响因子：
--
通讯作者：
Renato Silva;M. Butler
中科院分区：
文献类型：
--
作者：
Renato Silva;M. Butler
规范的构建通常是较小的子组件的组合。组合和分解是支持重用和允许通过细化步骤对子组件进行正式组合的技术。子组件可以由设计或体系结构目标产生，细化框架应该允许它们进一步开发，可能是并行的。我们建议在event - b形式化中定义组合和分解，遵循共享事件方法，其中子组件通过同步共享事件和共享状态进行交互是不允许的。我们定义了必要的证明义务，以确保有效的组合和分解。我们还证明了共享事件组合保留了精化证明，即为了保持组合的精化，在相应的子组件之间证明精化就足够了。本文使用Event-B工具集Rodin说明了应用这两种技术的案例研究。
The construction of specifications is often a combination of smaller sub-components.Compositionanddecompositionare techniques supporting reuse and allowing formal combination of sub-components through refinement steps. Sub-components can result from a design or architectural goal and a refinement framework should allow them to be further developed, possibly in parallel. We propose the definition of composition and decomposition in the Event-B formalism following a shared event approach where sub-components interact via synchronised shared events and shared states are not allowed. We define the necessary proof obligations to ensure valid compositions and decompositions. We also show that shared event composition preserves refinement proofs, that is, in order to maintain refinement of compositions, it is sufficient to prove refinement between corresponding sub-components. A case study applying these two techniques is illustrated using Rodin, the Event-B toolset.