Supporting Reuse of Event-B Developments through Generic Instantiation
Supporting Reuse of Event-B Developments through Generic Instantiation
复制标题
通过通用实例化支持事件 B 开发的重用
DOI：
10.1007/978-3-642-10373-5_24
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Butler
中科院分区：
文献类型：
--
作者：
Renato Silva;M. Butler
人们认为，在正式的开发中的可重用性应该减少在生产环境中的正式建模的时间和成本。沿着重用形式化模型的能力，在重用模型时避免不必要的重新证明是合乎需要的。Event-B是一种允许系统建模和细化的正式方法。事件B通过上下文构造支持泛型开发。然而，事件B缺乏在其他正式开发中实例化和重用通用开发的能力。我们提出了一种通用模型的实例化和扩展的实例化链的细化。我们定义了足够的证明义务，以确保与通用开发相关的证明在实例化开发中仍然有效，从而避免重新证明。
It is believed that reusability in formal development should reduce the time and cost of formal modelling within a production environment. Along with the ability to reuse formal models, it is desirable to avoid unnecessary re-proof when reusing models. Event-B is a formal method that allows modelling and refinement of systems. Event-B supports generic developments through the context construct. Nevertheless Event-B lacks the ability to instantiate and reuse generic developments in other formal developments. We propose a way of instantiating generic models and extending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development remain valid in an instantiated development thus avoiding re-proofs.