Search Results

Documents authored by Ingólfsdóttir, Anna

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.2
Runtime Instrumentation for Reactive Components

Authors: Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Reactive software calls for instrumentation methods that uphold the reactive attributes of systems. Runtime verification imposes another demand on the instrumentation, namely that the trace event sequences it reports to monitors are sound - that is, they reflect actual executions of the system under scrutiny. This paper presents RIARC, a novel decentralised instrumentation algorithm for outline monitors meeting these two demands. Asynchrony in reactive software complicates the instrumentation due to potential trace event loss or reordering. RIARC overcomes these challenges using a next-hop IP routing approach to rearrange and report events soundly to monitors. RIARC is validated in two ways. We subject its corresponding implementation to rigorous systematic testing to confirm its correctness. In addition, we assess this implementation via extensive empirical experiments, subjecting it to large realistic workloads to ascertain its reactiveness. Our results show that RIARC optimises its memory and scheduler usage to maintain latency feasible for soft real-time applications. We also compare RIARC to inline and centralised monitoring, revealing that it induces comparable latency to inline monitoring in moderate concurrency settings where software performs long-running, computationally-intensive tasks, such as in Big Data stream processing.
Cite as

Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir. Runtime Instrumentation for Reactive Components. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 2:1-2:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.ECOOP.2024.2,
  author =	{Aceto, Luca and Attard, Duncan Paul and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{Runtime Instrumentation for Reactive Components}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{2:1--2:33},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.2},
  URN =		{urn:nbn:de:0030-drops-208511},
  doi =		{10.4230/LIPIcs.ECOOP.2024.2},
  annote =	{Keywords: Runtime instrumentation, decentralised monitoring, reactive systems}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.1
Runtime Instrumentation for Reactive Components (Artifact)

Authors: Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Reactive software calls for instrumentation methods that uphold the reactive attributes of systems. Runtime verification sets another demand on the instrumentation, namely that the trace event sequences it reports to monitors are sound, i.e., they reflect actual executions of the system under scrutiny. Our companion paper, "Runtime Instrumentation for Reactive Components", presents RIARC, a novel decentralised instrumentation algorithm for outline monitors that meets these two demands. RIARC uses a next-hop IP routing approach to rearrange and report events soundly to monitors despite the potential trace event loss or reordering stemming from the asynchrony of reactive systems. The companion paper shows our corresponding RIARC Erlang implementation to be correct through rigorous systematic testing. We also assess RIARC via extensive empirical experiments, subjecting it to large realistic workloads in order to ascertain its reactiveness. This artefact packages the Erlang implementation, systematic tests that demonstrate its correctness, data sets obtained from our original empirical experiments detailed in the companion paper, and the scripts to rerun and replicate these results under lower workloads.
Cite as

Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir. Runtime Instrumentation for Reactive Components (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{aceto_et_al:DARTS.10.2.1,
  author =	{Aceto, Luca and Attard, Duncan Paul and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{Runtime Instrumentation for Reactive Components (Artifact)}},
  pages =	{1:1--1:4},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Aceto, Luca and Attard, Duncan Paul and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.1},
  URN =		{urn:nbn:de:0030-drops-208991},
  doi =		{10.4230/DARTS.10.2.1},
  annote =	{Keywords: Runtime instrumentation, decentralised monitoring, reactive systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.6
On the Axiomatisation of Branching Bisimulation Congruence over CCS

Authors: Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.
Cite as

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik. On the Axiomatisation of Branching Bisimulation Congruence over CCS. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2022.6,
  author =	{Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
  title =	{{On the Axiomatisation of Branching Bisimulation Congruence over CCS}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.6},
  URN =		{urn:nbn:de:0030-drops-170692},
  doi =		{10.4230/LIPIcs.CONCUR.2022.6},
  annote =	{Keywords: Equational basis, Weak semantics, CCS, Parallel composition}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.7
The Best a Monitor Can Do

Authors: Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Existing notions of monitorability for branching-time properties are fairly restrictive. This, in turn, impacts the ability to incorporate prior knowledge about the system under scrutiny - which corresponds to a branching-time property - into the runtime analysis. We propose a definition of optimal monitors that verify the best monitorable under- or over-approximation of a specification, regardless of its monitorability status. Optimal monitors can be obtained for arbitrary branching-time properties by synthesising a sound and complete monitor for their strongest monitorable consequence. We show that the strongest monitorable consequence of specifications expressed in Hennessy-Milner logic with recursion is itself expressible in this logic, and present a procedure to find it. Our procedure enables prior knowledge to be optimally incorporated into runtime monitors.
Cite as

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. The Best a Monitor Can Do. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2021.7,
  author =	{Aceto, Luca and Achilleos, Antonis and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{The Best a Monitor Can Do}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.7},
  URN =		{urn:nbn:de:0030-drops-134416},
  doi =		{10.4230/LIPIcs.CSL.2021.7},
  annote =	{Keywords: monitorability, branching-time logics, runtime verification}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.8
Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?

Authors: Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy’s merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. This study provides a negative answer to that question based on three reasonable assumptions.
Cite as

Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2021.8,
  author =	{Aceto, Luca and Castiglioni, Valentina and Fokkink, Wan and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
  title =	{{Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.8},
  URN =		{urn:nbn:de:0030-drops-134425},
  doi =		{10.4230/LIPIcs.CSL.2021.8},
  annote =	{Keywords: Equational logic, CCS, bisimulation, parallel composition, non-finitely based algebras}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.18
On the Axiomatisability of Parallel Composition: A Journey in the Spectrum

Authors: Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.
Cite as

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen. On the Axiomatisability of Parallel Composition: A Journey in the Spectrum. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2020.18,
  author =	{Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas and Pedersen, Mathias Ruggaard},
  title =	{{On the Axiomatisability of Parallel Composition: A Journey in the Spectrum}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{18:1--18:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.18},
  URN =		{urn:nbn:de:0030-drops-128303},
  doi =		{10.4230/LIPIcs.CONCUR.2020.18},
  annote =	{Keywords: Axiomatisation, Parallel composition, Linear time-branching time spectrum}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.34
On Runtime Enforcement via Suppressions

Authors: Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime. We study the enforceability of Hennessy-Milner Logic with Recursion (muHML) with respect to suppression enforcement. We develop an operational framework for enforcement which we then use to formalise when a monitor enforces a muHML property. We also show that the safety syntactic fragment of the logic, sHML, is enforceable by providing an automated synthesis function that generates correct suppression monitors from sHML formulas.
Cite as

Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir. On Runtime Enforcement via Suppressions. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2018.34,
  author =	{Aceto, Luca and Cassar, Ian and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{On Runtime Enforcement via Suppressions}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{34:1--34:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.34},
  URN =		{urn:nbn:de:0030-drops-95729},
  doi =		{10.4230/LIPIcs.CONCUR.2018.34},
  annote =	{Keywords: Enforceability, Suppression Enforcement, Monitor Synthesis, Logic}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.7
Monitoring for Silent Actions

Authors: Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
Silent actions are an essential mechanism for system modelling and specification. They are used to abstractly report the occurrence of computation steps without divulging their precise details, thereby enabling the description of important aspects such as the branching structure of a system. Yet, their use rarely features in specification logics used in runtime verification. We study monitorability aspects of a branching-time logic that employs silent actions, identifying which formulas are monitorable for a number of instrumentation setups. We also consider defective instrumentation setups that imprecisely report silent events, and establish monitorability results for tolerating these imperfections.
Cite as

Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. Monitoring for Silent Actions. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.FSTTCS.2017.7,
  author =	{Aceto, Luca and Achilleos, Antonis and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{Monitoring for Silent Actions}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{7:1--7:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.7},
  URN =		{urn:nbn:de:0030-drops-84023},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.7},
  annote =	{Keywords: Runtime Verification, Monitorability, Hennessy-Milner Logic with Recursion, Silent Actions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.10
Rule Formats for Nominal Process Calculi

Authors: Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, and Yolanda Ortega-Mallén

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specification of the early pi-calculus. Our study stems from the recent Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.
Cite as

Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, and Yolanda Ortega-Mallén. Rule Formats for Nominal Process Calculi. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2017.10,
  author =	{Aceto, Luca and F\'{a}bregas, Ignacio and Garc{\'\i}a-P\'{e}rez, \'{A}lvaro and Ing\'{o}lfsd\'{o}ttir, Anna and Ortega-Mall\'{e}n, Yolanda},
  title =	{{Rule Formats for Nominal Process Calculi}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.10},
  URN =		{urn:nbn:de:0030-drops-77869},
  doi =		{10.4230/LIPIcs.CONCUR.2017.10},
  annote =	{Keywords: nominal sets, nominal structural operational semantics, process algebra, nominal transition systems, scope opening, rule formats}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact