文章基本信息

标题：Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic
本地全文：下载
作者：Brijesh Dongol ; John Derrick ; Ian J. Hayes 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2013
卷号：53
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：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/guarantee-style 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.