DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2015.590

Failure-aware Runtime Verification of Distributed Systems

Authors: David Basin, Felix Klaedtke, and Eugen Zalinescu

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract

Prior runtime-verification approaches for distributed systems are limited as they do not account for network failures and they assume that system messages are received in the order they are sent. To overcome these limitations, we present an online algorithm for verifying observed system behavior at runtime with respect to specifications written in the real-time logic MTL that efficiently handles out-of-order message deliveries and operates in the presence of failures. Our algorithm uses a three-valued semantics for MTL, where the third truth value models knowledge gaps, and it resolves knowledge gaps as it propagates Boolean values through the formula structure. We establish the algorithm's soundness and provide completeness guarantees. We also show that it supports distributed system monitoring, where multiple monitors cooperate and exchange their observations and conclusions.

Cite as

David Basin, Felix Klaedtke, and Eugen Zalinescu. Failure-aware Runtime Verification of Distributed Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 590-603, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{basin_et_al:LIPIcs.FSTTCS.2015.590,
  author =	{Basin, David and Klaedtke, Felix and Zalinescu, Eugen},
  title =	{{Failure-aware Runtime Verification of Distributed Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{590--603},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.590},
  URN =		{urn:nbn:de:0030-drops-56194},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.590},
  annote =	{Keywords: Runtime verification, monitoring algorithm, real-time logics, multi-valued semantics, distributed systems, asynchronous communication}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2008.1740

Runtime Monitoring of Metric First-order Temporal Properties

Authors: David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract

We introduce a novel approach to the runtime monitoring of complex system properties. In particular, we present an online algorithm for a safety fragment of metric first-order temporal logic that is considerably more expressive than the logics supported by prior monitoring methods. Our approach, based on automatic structures, allows the unrestricted use of negation, universal and existential quantification over infinite domains, and the arbitrary nesting of both past and bounded future operators. Moreover, we show how to optimize our approach for the common case where structures consist of only finite relations, over possibly infinite domains. Under an additional restriction, we prove that the space consumed by our monitor is polynomially bounded by the cardinality of the data appearing in the processed prefix of the temporal structure being monitored.

Cite as

David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann. Runtime Monitoring of Metric First-order Temporal Properties. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 49-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{basin_et_al:LIPIcs.FSTTCS.2008.1740,
  author =	{Basin, David and Klaedtke, Felix and M\"{u}ller, Samuel and Pfitzmann, Birgit},
  title =	{{Runtime Monitoring of Metric First-order Temporal Properties}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{49--60},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1740},
  URN =		{urn:nbn:de:0030-drops-17404},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1740},
  annote =	{Keywords: Runtime Monitoring, Metric First-order Temporal Logic, Automatic Structures, Temporal Databases}
}

Document

DOI: 10.4230/LIPIcs.STACS.2008.1364

Ehrenfeucht-Fraissé Goes Automatic for Real Addition

Authors: Felix Klaedtke

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract

Various logical theories can be decided by automata-theoretic methods. Notable examples are Presburger arithmetic FO$(Z,+,<)$ and the linear arithmetic over the reals FO$(R,+,<)$, for which effective decision procedures can be built using automata. Despite the practical use of automata to decide logical theories, many research questions are still only partly answered in this area. One of these questions is the complexity of such decision procedures and the related question about the minimal size of the automata of the languages that can be described by formulas in the respective logic. In this paper, we establish a double exponential upper bound on the automata size for FO$(R,+,<)$ and an exponential upper bound for the discrete order over the integers FO$(Z,<)$. The proofs of these upper bounds are based on Ehrenfeucht-Fraiss{'\e} games. The application of this mathematical tool has a similar flavor as in computational complexity theory, where it can often be used to establish tight upper bounds of the decision problem for logical theories.

Cite as

Felix Klaedtke. Ehrenfeucht-Fraissé Goes Automatic for Real Addition. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 445-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{klaedtke:LIPIcs.STACS.2008.1364,
  author =	{Klaedtke, Felix},
  title =	{{Ehrenfeucht-Fraiss\'{e}  Goes Automatic for Real Addition}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{445--456},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1364},
  URN =		{urn:nbn:de:0030-drops-13649},
  doi =		{10.4230/LIPIcs.STACS.2008.1364},
  annote =	{Keywords: Automata theory, automata-based decision procedures for logical theories, upper bounds, minimal sizes of automata, linear arithmetic over the reals, f}
}

3 Search Results for "Klaedtke, Felix"

Failure-aware Runtime Verification of Distributed Systems

Abstract

Cite as

Runtime Monitoring of Metric First-order Temporal Properties

Abstract

Cite as

Ehrenfeucht-Fraissé Goes Automatic for Real Addition

Abstract

Cite as

Thanks for your feedback!

Could not send message