Please use this identifier to cite or link to this item:
http://bura.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 | Size | Format | |
---|---|---|---|---|
Fulltext.pdf | 214.64 kB | Adobe PDF | View/Open |
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.