Electronic Communications of the EASST Volume 53 ( 2012 ) Proceedings of the 12 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2012 ) Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic
Electronic Communications of the EASST Volume 53 ( 2012 ) Proceedings of the 12 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2012 ) Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic
复制标题
EASST 电子通信第 53 卷 (2012) 第 12 届关键系统自动验证国际研讨会论文集 (AVoCS 2012) 区间时间逻辑中的分数权限和非确定性评估器
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
I. Hayes
中科院分区：
文献类型：
--
作者：
Brijesh Dongol;J. Derrick;I. Hayes
我们建议区间时态逻辑作为推理的基础上并发程序的细粒度原子性，由于它提供了超过推理与标准的前/后状态关系的一般性。为了简化间隔上的并行组合的语义，我们使用分数权限，这允许一个确保冲突的读取和写入一个变量不会同时发生。使用非确定性评估器的间隔，我们使推理的明显状态的间隔，这可能不同于实际状态的间隔。区间时态逻辑，非确定性评估器和分数权限的组合结果在一个通用的框架推理并发程序与细粒度原子性。我们使用我们的逻辑来开发依赖/依赖风格规则，用于将大型系统的证明分解为其子组件的证明，其中使用分数权限来确保程序及其环境的行为不冲突。
We propose Interval Temporal Logic as a basis for reasoning about concurrent programs with fine-grained atomicity due to the generality it provides over reasoning with standard pre/post-state relations. To simplify the semantics of parallel composition over intervals, we use fractional permissions, which allows one to ensure that conflicting reads and writes to a variable do not occur simultaneously. Using non-deterministic evaluators over intervals, we enable reasoning about the apparent states over an interval, which may differ from the actual states in the interval. The combination of Interval Temporal Logic, non-deterministic evaluators and fractional permissions results in a generic framework for reasoning about concurrent programs with fine-grained atomicity. We use our logic to develop rely/guaranteestyle rules for decomposing a proof of a large system into proofs of its subcomponents, where fractional permissions are used to ensure that the behaviours of a program and its environment do not conflict.