hh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Avoiding Diamonds in Desynchronisation
Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands.
2014 (Engelska)Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 91, nr PART A, s. 45-69Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
Amsterdam: Elsevier, 2014. Vol. 91, nr PART A, s. 45-69
Nyckelord [en]
Synchrony to asynchrony, Desynchronisation, Branching bisimulation, Equivalence checking of infinite state systems
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:hh:diva-24984DOI: 10.1016/j.scico.2013.12.002ISI: 000338401300003Scopus ID: 2-s2.0-84901613572OAI: oai:DiVA.org:hh-24984DiVA, id: diva2:710254
Konferens
9th International Symposium on Formal Aspects of Component Software (FACS), Mountain View, CA, USA, September 12-14, 2012
Projekt
“Integrated Multi-formalism Tool Support for the Design of Networked Embedded Control Systems” (MULTIFORM) project
Forskningsfinansiär
EU, FP7, Sjunde ramprogrammet, INFSO-ICT-224249Tillgänglig från: 2014-04-05 Skapad: 2014-04-05 Senast uppdaterad: 2018-03-22Bibliografiskt granskad

Open Access i DiVA

hb-scp-2014(332 kB)153 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 332 kBChecksumma SHA-512
78bb26b15ece96b34fb55e4bc5be3a8e4f7ad229560ade6fd6f2a86258c0a06dd8bf7894237afe2e2cadd2eb276838faa97f76db687f77bc86f1cf3878ab76d6
Typ fulltextMimetyp application/pdf

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Beohar, Harsh

Sök vidare i DiVA

Av författaren/redaktören
Beohar, Harsh
Av organisationen
Centrum för forskning om inbyggda system (CERES)
I samma tidskrift
Science of Computer Programming
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 153 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 508 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf