Relational Concurrent Refinement
Relational Concurrent Refinement
复制标题
关系并发细化
DOI：
10.1007/s00165-003-0007-4
复制
发表时间：
2003
影响因子：
1
通讯作者：
E. Boiten
中科院分区：
文献类型：
--
作者：
J. Derrick;E. Boiten
并发上下文中的细化，以进程代数为代表，根据被认为是可观察的内容，采取许多不同的形式。例如，观察记录系统准备接受或拒绝哪些事件。并发求精关系包括跟踪求精、故障-发散求精、就绪求精和互模拟。另一方面，Z等基于状态的语言中的细化是使用关系模型根据抽象程序的输入输出行为定义的。这些改进通常通过使用两个模拟规则来验证，这有助于使验证易于处理。本文统一了这两个观点，概括了标准的关系模型，包括额外的可观察到的方面。这些被选择在这样一种方式，他们代表的观察嵌入在各种并发的细化关系的概念。因此，可以推导出并发精化的易处理验证的模拟规则。我们开发这样的模拟规则的故障分歧细化和准备细化，特别是在后一种情况下，使用一种替代的关系模型。
Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable. Observations record, for example, which events a system is prepared to accept or refuse. Concurrent refinement relations include trace refinement, failures–divergences refinement, readiness refinement and bisimulation. Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of the input–output behaviour of abstract programs. These refinements are normally verified by using two simulation rules which help make the verification tractable. This paper unifies these two standpoints by generalising the standard relational model to include additional observable aspects. These are chosen in such a way that they represent exactly the notions of observation embedded in the various concurrent refinement relations. As a consequence, simulation rules for the tractable verification of concurrent refinement can be derived. We develop such simulation rules for failures–divergences refinement and readiness refinement in particular, using an alternative relational model in the latter case.