DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2022.6

Decentralised Runtime Verification of Timed Regular Expressions

Authors: Victor Roussanaly and Yliès Falcone

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

Abstract

Ensuring the correctness of distributed cyber-physical systems can be done at runtime by monitoring properties over their behaviour. In a decentralised setting, such behaviour consists of multiple local traces, each offering an incomplete view of the system events to the local monitors, as opposed to the standard centralised setting with a unique global trace. We introduce the first monitoring framework for timed properties described by timed regular expressions over a distributed network of monitors. First, we define functions to rewrite expressions according to partial knowledge for both the centralised and decentralised cases. Then, we define decentralised algorithms for monitors to evaluate properties using these functions, as well as proofs of soundness and eventual completeness of said algorithms. Finally, we implement and evaluate our framework on synthetic timed regular expressions, giving insights on the cost of the centralised and decentralised settings and when to best use each of them.

Cite as

Victor Roussanaly and Yliès Falcone. Decentralised Runtime Verification of Timed Regular Expressions. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{roussanaly_et_al:LIPIcs.TIME.2022.6,
  author =	{Roussanaly, Victor and Falcone, Yli\`{e}s},
  title =	{{Decentralised Runtime Verification of Timed Regular Expressions}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.6},
  URN =		{urn:nbn:de:0030-drops-172532},
  doi =		{10.4230/LIPIcs.TIME.2022.6},
  annote =	{Keywords: Timed expressions, Timed properties, Monitoring, Runtime verification, Decentralized systems, Asynchronous communication}
}

Search Results

Documents authored by Falcone, Yliès

Decentralised Runtime Verification of Timed Regular Expressions

Abstract

Cite as

Thanks for your feedback!

Could not send message