Change search
ReferencesLink to record
Permanent link

Direct link
Avoiding Diamonds in Desynchronisation
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).
Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands.
2014 (English)In: Science of Computer Programming, ISSN 0167-6423, Vol. 91, no PART A, 45-69 p.Article in journal (Refereed) Published
Abstract [en]

The design of concurrent systems often assumes synchronous communication between different parts of a system. When system components are physically apart, this assumption becomes inappropriate. Desynchronisation is a technique that aims to implement a synchronous design in an asynchronous manner by placing buffers between the components of the synchronous design. When queues are used as buffers, the so-called 'diamond property' (among others) ensures correct operation of the desynchronised design. However, this property is difficult to establish in practice. In this paper, we give sufficient and necessary conditions under which a concrete synchronous design (i.e., without the unobservable action) is equivalent to an asynchronous design and formally prove that the diamond property is no longer needed for desynchronisation when half-duplex queues are used as a communication buffer. Furthermore, we discuss how the half-duplex condition can be further relaxed when the diamond property can be partially guaranteed. To illustrate how this theory may be applied, we desynchronise the synchronous systems that are synthesised using supervisory control theory. © 2013 Elsevier B.V.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2014. Vol. 91, no PART A, 45-69 p.
Keyword [en]
Synchrony to asynchrony, Desynchronisation, Branching bisimulation, Equivalence checking of infinite state systems
National Category
Computer Science
URN: urn:nbn:se:hh:diva-24984DOI: 10.1016/j.scico.2013.12.002ISI: 000338401300003ScopusID: 2-s2.0-84901613572OAI: diva2:710254
9th International Symposium on Formal Aspects of Component Software (FACS), Mountain View, CA, USA, September 12-14, 2012
“Integrated Multi-formalism Tool Support for the Design of Networked Embedded Control Systems” (MULTIFORM) project
EU, FP7, Seventh Framework Programme, INFSO-ICT-224249
Available from: 2014-04-05 Created: 2014-04-05 Last updated: 2015-01-12Bibliographically approved

Open Access in DiVA

hb-scp-2014(332 kB)35 downloads
File information
File name FULLTEXT01.pdfFile size 332 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Beohar, Harsh
By organisation
Centre for Research on Embedded Systems (CERES)
In the same journal
Science of Computer Programming
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 35 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 161 hits
ReferencesLink to record
Permanent link

Direct link