Foundations for using linear temporal logic in Event-B refinement
Foundations for using linear temporal logic in Event-B refinement
复制标题
在事件 B 细化中使用线性时序逻辑的基础
DOI：
10.1007/s00165-016-0376-0
复制
发表时间：
2016
影响因子：
1
通讯作者：
David M. Williams
中科院分区：
文献类型：
--
作者：
Son Hoang;Steve A. Schneider;H. Treharne;David M. Williams
在本文中，我们提出了一种协调事件 B 细化与线性时序逻辑 (LTL) 属性的新方法。特别是，本文提出的结果允许为抽象系统模型建立属性，并确定条件以确保在通过细化开发这些模型时，属性（适当翻译）继续保持。这一成就有几个新颖的元素：（1）我们确定了允许 LTL 属性跨细化链映射的条件； （2）我们提供LTL谓词的翻译，以反映新事件的细化引入以及现有事件的重命名和拆分； (3) 我们这样做是为了 LTL 的扩展版本，特别适合 Event-B，包括状态谓词和事件的启用性，可以在抽象级别进行模型检查。我们的结果比该领域之前的任何工作都更加普遍，涵盖了预期事件背景下的活跃度，并放松了相邻细化级别之间的限制。该方法通过案例研究进行说明。这使得设计人员能够开发基于事件的模型并考虑其执行模式，以便可以验证事件 B 系统的活性和公平性属性。
In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.