Compositional Action System Derivation Using Enforced Properties
Compositional Action System Derivation Using Enforced Properties
复制标题
使用强制属性推导组合动作系统
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
I. Hayes
中科院分区：
文献类型：
--
作者：
Brijesh Dongol;I. Hayes
行动系统已被证明适用于建模和构建顺序系统和并发系统。本文提出了一种程序构造方法，其中具体实现源自其规范——通过一系列小的改进——使用不完整的证明来激发对程序的更改。我们的方法的形式化是由强制属性提供的，它将程序的跟踪限制为满足强制属性的跟踪。推导的目标是将具有强制属性的程序细化为代码满足强制属性的程序（没有强制属性）。这种方法的一个优点是程序早期版本中的代码不需要完整；通过在规范中包含强制属性可以避免程序的错误执行。强制属性可以是任何时间公式或关系，因此我们可以在组合设置中推理安全性和进度。
Action systems have been shown to be applicable for modelling and constructing both sequential and concurrent systems. This paper presents an approach to program construction where the concrete implementation is derived from its specification -- via a series of small refinements -- using incomplete proofs to motivate changes to the program. Formalisation of our approach is provided by enforced properties, which restrict the traces of a program to those that satisfy the enforced properties. The goal of the derivation is to refine a program with enforced properties to a program (with no enforced properties) whose code satisfies the enforced properties. An advantage of this approach is that the code in the earlier versions of the program need not be complete; incorrect execution of the program is avoided by including enforced properties in the specification. Enforced properties may be any temporal formula or relation, and hence we may reason about both safety and progress in a compositional setting.
DOI：
10.1007/978-3-642-00867-2
发表时间：
2009-03
期刊：
--
影响因子：
--
作者：
M. Butler;Cliff B. Jones;A. Romanovsky;E. Troubitsyna
通讯作者：
M. Butler;Cliff B. Jones;A. Romanovsky;E. Troubitsyna