Slow Abstraction via Priority
Slow Abstraction via Priority
复制标题
通过优先级缓慢抽象
DOI：
10.1007/978-3-642-39698-4_20
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Philippa J. Hopcroft
中科院分区：
文献类型：
--
作者：
A. W. Roscoe;Philippa J. Hopcroft
CSP将内部τ作用视为紧急的，因此它们的无限序列是被称为散度的错误行为，并且有它们可用的状态没有我们可以依赖的报价。虽然有可能在这些模型中形成一些抽象形式，其中抽象的动作成为τs，但有时有必要小心解释τs和散度。在本文中，受一个工业问题的启发，我们演示了如何将这一抽象范围扩展到包含在“慢τs”运行期间由过程提出的报价，即与外部代理的交互的抽象，该代理通常不紧急响应报价，但最终总是响应。这种扩展需要最近引入CSP及其改进检查器FDR的优先级操作符。我们在Verum的ASD:Suite中演示了它在建模中的使用。
CSP treats internal τ actions as urgent, so that an infinite sequence of them is the misbehaviour known as divergence, and states with them available make no offer that we can rely on. While it has been possible to formulate a number of forms of abstraction in these models where the abstracted actions become τs, it has sometimes been necessary to be careful about the interpretation of τs and divergence. In this paper, inspired by an industrial problem, we demonstrate how this range of abstractions can be extended to encompass the offers made by processes during a run of "slow τs", namely abstractions of interactions with an external agent that does not usually respond urgently to an offer, but always eventually does respond. This extension requires the prioritise operator recently introduced into CSP and its refinement checker FDR. We demonstrate its use in the modelling used in Verum's ASD:Suite.