Please use this identifier to cite or link to this item: http://buratest.brunel.ac.uk/handle/2438/11251
Title: Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems
Authors: Dongol, B
Derrick, J
Keywords: Refinement;Interval-based reasoning;True concurrency;Discrete time systems;Real-time systems
Issue Date: 2014
Publisher: Elsevier
Citation: Science of Computer Programming, 2014
Abstract: The majority of modern systems exhibit sophisticated concurrent behaviour, where several system components observe and modify the state with fine-grained atomicity. Many systems also exhibit truly concurrent behaviour, where multiple events may occur simultaneously. Data refinement, a correctness criterion to compare an abstract and a concrete implementation, normally admits interleaved models of execution only. In this paper, we present a method of data refinement using a framework that allows one to view a component's evolution over an interval of time, simplifying reasoning about true concurrency. By modifying the type of an interval, our theory may be specialised to cover data refinement of both discrete and real-time systems. We develop a sound interval-based forward simulation rule that enables decomposition of data refinement proofs, and apply this rule to verify data refinement for two examples: a simple concurrent program and a more in-depth real-time controller.
URI: http://www.sciencedirect.com/science/article/pii/S016764231500101X
http://bura.brunel.ac.uk/handle/2438/11251
DOI: http://dx.doi.org/10.1016/j.scico.2015.05.005
ISSN: 0167-6423
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Fulltext.pdf564.92 kBAdobe PDFView/Open


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