Data refinement for true concurrency
Data refinement for true concurrency
复制标题
数据细化实现真正的并发
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
J. Derrick
中科院分区：
文献类型：
--
作者：
Brijesh Dongol;J. Derrick
大多数现代系统表现出复杂的并发行为，其中多个系统组件以细粒度原子性修改和观察系统状态。许多系统(例如，多核处理器、实时控制器)也表现出真正的并发行为，其中多个事件可以同时发生。本文提出了一种基于区间的数据求精框架，该框架包括捕获非确定性表达式求值的高级操作符。通过修改区间的类型，我们的理论可以专门涵盖离散和连续系统的数据精化。我们提出了一种基于区间的前向模拟编码，并证明了我们的前向模拟规则相对于我们的数据精化定义是合理的。给出了顺序合成和并行合成的正演模拟证明分解规则。
The majority of modern systems exhibit sophisticated concurrent behaviour, where several system components modify and observe the system state with fine-grained atomicity. Many systems (e.g., multi-core processors, real-time controllers) also exhibit truly concurrent behaviour, where multiple events can occur simultaneously. This paper presents data refinement defined in terms of an interval-based framework, which includes high-level operators that capture non-deterministic expression evaluation. By modifying the type of an interval, our theory may be specialised to cover data refinement of both discrete and continuous systems. We present an interval-based encoding of forward simulation, then prove that our forward simulation rule is sound with respect to our data refinement definition. A number of rules for decomposing forward simulation proofs over both sequential and parallel composition are developed.
比较表达式评估中的非决定论程度
DOI：
10.1093/comjnl/bxt005
发表时间：
2013
期刊：
The Computer Journal
影响因子：
--
作者：
Hayes I
通讯作者：
Hayes I