Please use this identifier to cite or link to this item: http://buratest.brunel.ac.uk/handle/2438/9224
Title: Data refinement for true concurrency
Authors: Dongol, B
Derrick, J
Keywords: Logic in Computer Science;State-based data refinement;Interval-based reasoning;Interval relations;Generalised forward simulation;Fine-grained atomicity
Issue Date: 2013
Publisher: Electronic Proceedings in Theoretical Computer Science, 16th International Refinement Workshop
Citation: EPTCS 115(2013): 15-35, Jun 2013
Abstract: 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.
URI: http://arxiv.org/abs/1305.6111v1
http://bura.brunel.ac.uk/handle/2438/9224
DOI: http://dx.doi.org/10.4204/EPTCS.115.2
Appears in Collections:Computer Science
Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf214.64 kBAdobe PDFView/Open


Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.