Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems
Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems
复制标题
基于间隔的数据细化：在离散和实时系统中实现真正并发的统一方法
DOI：
10.1016/j.scico.2015.05.005
复制
发表时间：
2015
影响因子：
1.3
通讯作者：
Dongol B
中科院分区：
文献类型：
--
作者：
Dongol B
大多数现代系统都表现出复杂的并发行为，其中多个系统组件以细粒度的原子性观察和修改状态。许多系统还表现出真正的并发行为，其中多个事件可能同时发生。数据细化是比较抽象和具体实现的正确性标准，通常只允许交叉执行模型。在本文中，我们提出了一种方法，使用一个框架，允许查看一个组件的演变在一段时间内，简化推理真正的并发性的数据细化。通过修改间隔的类型，我们的理论可以专门涵盖离散和实时系统的数据细化。我们开发了一个健全的基于区间的前向模拟规则，使分解的数据细化证明，并应用此规则来验证数据细化两个例子：一个简单的并发程序和更深入的实时控制器。
The majority of modern systems exhibit sophisticated concurrent behaviour, where several system components observe and modify the state with fine-grained atomicity. Many systems also exhibit truly concurrent behaviour, where multiple events may occur simultaneously. Data refinement, a correctness criterion to compare an abstract and a concrete implementation, normally admits interleaved models of execution only. In this paper, we present a method of data refinement using a framework that allows one to view a component's evolution over an interval of time, simplifying reasoning about true concurrency. By modifying the type of an interval, our theory may be specialised to cover data refinement of both discrete and real-time systems. We develop a sound interval-based forward simulation rule that enables decomposition of data refinement proofs, and apply this rule to verify data refinement for two examples: a simple concurrent program and a more in-depth real-time controller.
登录
查看更多内容
数据细化实现真正的并发
DOI：
--
发表时间：
2013
期刊：
Refine@IFM
影响因子：
--
作者：
Brijesh Dongol;J. Derrick
通讯作者：
J. Derrick
具有依赖/保证条件的原子分裂以及数据具体化
DOI：
--
发表时间：
2008
期刊：
International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z
影响因子：
--
作者：
Cliff B. Jones;K. G. Pierce
通讯作者：
K. G. Pierce
EASST 电子通信第 53 卷 (2012) 第 12 届关键系统自动验证国际研讨会论文集 (AVoCS 2012) 区间时间逻辑中的分数权限和非确定性评估器
DOI：
--
发表时间：
2012
期刊：
影响因子：
--
作者：
Brijesh Dongol;J. Derrick;I. Hayes
通讯作者：
I. Hayes
一种多道程序设计方法
DOI：
--
发表时间：
2010
期刊：
Monographs in Computer Science
影响因子：
--
作者：
David Gries;Fred B. Schneider
通讯作者：
Fred B. Schneider
EASST 电子通信第 66 卷 (2013) 关键系统自动验证论文集 (AVoCS 2013) 使用抽象层简化线性化证明
DOI：
--
发表时间：
2014
期刊：
影响因子：
--
作者：
Brijesh Dongol;J. Derrick
通讯作者：
J. Derrick