License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2018.40
URN: urn:nbn:de:0030-drops-95786
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9578/
Go to the corresponding LIPIcs Volume Portal

Bartoletti, Massimo ; Bocchi, Laura ; Murgia, Maurizio

Progress-Preserving Refinements of CTA

pdf-format:
LIPIcs-CONCUR-2018-40.pdf (0.6 MB)

Abstract

We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints - in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems, such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.

BibTeX - Entry

@InProceedings{bartoletti_et_al:LIPIcs:2018:9578,
  author =	{Massimo Bartoletti and Laura Bocchi and Maurizio Murgia},
  title =	{{Progress-Preserving Refinements of CTA}},
  booktitle =	{29th International Conference on Concurrency Theory  (CONCUR 2018)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Sven Schewe and Lijun Zhang},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9578},
  URN =		{urn:nbn:de:0030-drops-95786},
  doi =		{10.4230/LIPIcs.CONCUR.2018.40},
  annote =	{Keywords: protocol implementation, communicating timed automata, message passing}
}

Keywords: protocol implementation, communicating timed automata, message passing
Collection: 29th International Conference on Concurrency Theory (CONCUR 2018)
Issue Date: 2018
Date of publication: 31.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI