DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2023.6

Bounded-Memory Runtime Enforcement of Timed Properties

Authors: Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract

Runtime Enforcement (RE) is a monitoring technique aimed at correcting possibly incorrect executions w.r.t. a set of formal requirements (properties) of a system. In this paper, we consider enforcement monitoring of real-time properties. Thus, executions are modelled as timed words and specifications as timed automata. Moreover, we consider that the enforcer has the ability to delay events by storing or buffering them into its internal memory (and releasing them when the property is finally satisfied) and suppressing events when no delaying is appropriate. Practically, in an implementation, the internal memory of the enforcer is finite. In this paper, we propose a new RE paradigm for timed properties, where the memory of the enforcer is bounded/finite, to address practical applications with memory constraints and timed specifications. Bounding the memory presents a number of difficulties, e.g., how to accommodate a timed event into the memory when the memory is full, s.t., regardless of the course of action we choose to handle this situation, the behaviour of the bounded enforcer should not significantly differ from that of the unbounded enforcer. The problem of how to optimally discard events when the buffer is full is significantly more difficult in a timed environment where the progress of time affects the satisfaction or violation of a property. We define the bounded-memory RE problem for timed properties and develop a framework for regular timed properties specified as timed automata. The proposed framework is implemented in Python, and its performance is evaluated. From experiments, we discovered that the enforcer has a reasonable execution time overhead.

Cite as

Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron. Bounded-Memory Runtime Enforcement of Timed Properties. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{shankar_et_al:LIPIcs.TIME.2023.6,
  author =	{Shankar, Saumya and Pinisetty, Srinivas and J\'{e}ron, Thierry},
  title =	{{Bounded-Memory Runtime Enforcement of Timed Properties}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.6},
  URN =		{urn:nbn:de:0030-drops-190962},
  doi =		{10.4230/LIPIcs.TIME.2023.6},
  annote =	{Keywords: Formal methods, Runtime enforcement, Bounded-memory, Timed automata}
}

Document

DOI: 10.4230/DagRep.3.1.1

Symbolic Methods in Testing (Dagstuhl Seminar 13021)

Authors: Thierry Jéron, Margus Veanes, and Burkhart Wolff

Published in: Dagstuhl Reports, Volume 3, Issue 1 (2013)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 13021 "Symbolic Methods in Testing". The aim of the seminar was to bring together leading researchers of this field; the seminary ended up with 38 participants from 10 countries: France, The Netherlands, The Unites States, Germany, Switzerland, United Kingdom, Brazil, Norway, Estonia and Italy. Through a series of presentations, discussions, and working group meetings, the seminar attempted to get a coherent picture of the field, which transcends the borders of applications and disciplines, of existing approaches and problems in formal testing. The seminar brought together, on the one hand, researchers from the different camps and various tools. The main outcome of the seminar is the exchange of information between different groups and the discussion of new trends (parallelization, cloud-computing).

Cite as

Thierry Jéron, Margus Veanes, and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021). In Dagstuhl Reports, Volume 3, Issue 1, pp. 1-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{jeron_et_al:DagRep.3.1.1,
  author =	{J\'{e}ron, Thierry and Veanes, Margus and Wolff, Burkhart},
  title =	{{Symbolic Methods in Testing (Dagstuhl Seminar 13021)}},
  pages =	{1--29},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{1},
  editor =	{J\'{e}ron, Thierry and Veanes, Margus and Wolff, Burkhart},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.1.1},
  URN =		{urn:nbn:de:0030-drops-40060},
  doi =		{10.4230/DagRep.3.1.1},
  annote =	{Keywords: Automated Deduction, White-box testing, Black-box Testing, Fuzz-Testing, Unit-Testing,Theorem prover-based Testing}
}

Search Results

Documents authored by Jéron, Thierry

Bounded-Memory Runtime Enforcement of Timed Properties

Abstract

Cite as

Symbolic Methods in Testing (Dagstuhl Seminar 13021)

Abstract

Cite as

Thanks for your feedback!

Could not send message