Data refinement for true concurrency

Brijesh Dongol
(The University of Sheffield)
John Derrick
(The University of Sheffield)

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.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 16th International Refinement Workshop (Refine 2013), Turku, Finland, 11th June 2013, Electronic Proceedings in Theoretical Computer Science 115, pp. 15–35.
Published: 24th May 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.115.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org