Fractional permissions and non-deterministic evaluators in interval temporal logic

Dongol, Brijesh, Derrick, John and Hayes, Ian J. (2012). Fractional permissions and non-deterministic evaluators in interval temporal logic. In: Gerald Luettgen and Stephan Merz, Automated Verification of Critical Systems 2012. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Bamberg, Germany, (1-15). 18–20 September 2012.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
UQ294230_OA.pdf Full text (open access) application/pdf 191.55KB 0
Author Dongol, Brijesh
Derrick, John
Hayes, Ian J.
Title of paper Fractional permissions and non-deterministic evaluators in interval temporal logic
Conference name 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012)
Conference location Bamberg, Germany
Conference dates 18–20 September 2012
Proceedings title Automated Verification of Critical Systems 2012   Check publisher's open access policy
Journal name Electronic Communications of the EASST   Check publisher's open access policy
Place of Publication Berlin, Germany
Publisher European Association of Software Science and Technology (E A S S T)
Publication Year 2012
Sub-type Fully published paper
Open Access Status File (Publisher version)
ISSN 1863-2122
Editor Gerald Luettgen
Stephan Merz
Volume 53
Start page 1
End page 15
Total pages 15
Collection year 2013
Language eng
Abstract/Summary 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.
Keyword Interval temporal logic
Fractional permissions
Non-deterministic expression evaluation
Parallel composition
Compositional reasoning
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Google Scholar Search Google Scholar
Created: Tue, 19 Mar 2013, 17:02:19 EST by Ian Hayes on behalf of School of Information Technol and Elec Engineering