13 Search Results for "Francalanza, Adrian"

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
DOI: 10.4230/LIPIcs.ECOOP.2024.4
Dynamically Generating Callback Summaries for Enhancing Static Analysis

Authors: Steven Arzt, Marc Miltenberger, and Julius Näumann

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

Abstract
Interprocedural static analyses require a complete and precise callgraph. Since third-party libraries are responsible for large portions of the code of an app, a substantial fraction of the effort in callgraph generation is therefore spent on the library code for each app. For analyses that are oblivious to the inner workings of a library and only require the user code to be processed, the library can be replaced with a summary that allows to reconstruct the callbacks from library code back to user code. To improve performance, we propose the automatic generation and use of precise pre-computed callgraph summaries for commonly used libraries. Reflective method calls within libraries and callback-driven APIs pose further challenges for generating precise callgraphs using static analysis. Pre-computed summaries can also help analyses avoid these challenges. We present CGMiner, an approach for automatically generating callgraph models for library code. It dynamically observes sample apps that use one or more particular target libraries. As we show, CGMiner yields more than 94% of correct edges, whereas existing work only achieves around 33% correct edges. CGMiner avoids the high false positive rate of existing tools. We show that CGMiner integrated into FlowDroid uncovers 40% more data flows than our baseline without callback summaries.
Cite as

Steven Arzt, Marc Miltenberger, and Julius Näumann. Dynamically Generating Callback Summaries for Enhancing Static Analysis. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arzt_et_al:LIPIcs.ECOOP.2024.4,
  author =	{Arzt, Steven and Miltenberger, Marc and N\"{a}umann, Julius},
  title =	{{Dynamically Generating Callback Summaries for Enhancing Static Analysis}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{4:1--4:27},
  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.4},
  URN =		{urn:nbn:de:0030-drops-208533},
  doi =		{10.4230/LIPIcs.ECOOP.2024.4},
  annote =	{Keywords: dynamic analysis, callback detection, java, android}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.5
Behavioural Up/down Casting For Statically Typed Languages

Authors: Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara

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

Abstract
We provide support for polymorphism in static typestate analysis for object-oriented languages with upcasts and downcasts. Recent work has shown how typestate analysis can be embedded in the development of Java programs to obtain safer behaviour at runtime, e.g., absence of null pointer errors and protocol completion. In that approach, inheritance is supported at the price of limiting casts in source code, thus only allowing those at the beginning of the protocol, i.e., immediately after objects creation, or at the end, and in turn seriously affecting the applicability of the analysis. In this paper, we provide a solution to this open problem in typestate analysis by introducing a theory based on a richer data structure, named typestate tree, which supports upcast and downcast operations at any point of the protocol by leveraging union and intersection types. The soundness of the typestate tree-based approach has been mechanised in Coq. The theory can be applied to most object-oriented languages statically analysable through typestates, thus opening new scenarios for acceptance of programs exploiting inheritance and casting. To defend this thesis, we show an application of the theory, by embedding the typestate tree mechanism in a Java-like object-oriented language, and proving its soundness.
Cite as

Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, and António Ravara. Behavioural Up/down Casting For Statically Typed Languages. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bacchiani_et_al:LIPIcs.ECOOP.2024.5,
  author =	{Bacchiani, Lorenzo and Bravetti, Mario and Giunti, Marco and Mota, Jo\~{a}o and Ravara, Ant\'{o}nio},
  title =	{{Behavioural Up/down Casting For Statically Typed Languages}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{5:1--5:28},
  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.5},
  URN =		{urn:nbn:de:0030-drops-208543},
  doi =		{10.4230/LIPIcs.ECOOP.2024.5},
  annote =	{Keywords: Behavioural types, object-oriented programming, subtyping, cast, typestates}
}
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.2024.4
Centralized vs Decentralized Monitors for Hyperproperties

Authors: Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.
Cite as

Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker. Centralized vs Decentralized Monitors for Hyperproperties. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2024.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Anastasiadi, Elli and Francalanza, Adrian and Gorla, Daniele and Wagemaker, Jana},
  title =	{{Centralized vs Decentralized Monitors for Hyperproperties}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.4},
  URN =		{urn:nbn:de:0030-drops-207763},
  doi =		{10.4230/LIPIcs.CONCUR.2024.4},
  annote =	{Keywords: Runtime Verification, hyperlogics, decentralization}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2024.2
SlackCheck: A Linux Kernel Module to Verify Temporal Properties of a Task Schedule

Authors: Michele Castrovilli and Enrico Bini

Published in: LIPIcs, Volume 298, 36th Euromicro Conference on Real-Time Systems (ECRTS 2024)

Abstract
The Linux Kernel offers several scheduling classes. From SCHED_DEADLINE down to SCHED_FIFO, SCHED_RR and SCHED_OTHER, the scheduling classes can provide different responsiveness to very diverse user workloads. Still, Linux does not offer any mechanism to take some action upon the violation of temporal constraints at runtime. The lack of such a feature is also due to the difficulty of extending the established notion of deadline to workloads which are not releasing periodic/sporadic jobs. Exploiting the notion of supply functions for any resource schedule, we implemented SlackCheck, a kernel module which is capable to verify at runtime if a given task is assigned a desired amount of resource or not. SlackCheck adds a constant-time check at every scheduling decision and leverages the recent availability of a Runtime Verification engine in the kernel.
Cite as

Michele Castrovilli and Enrico Bini. SlackCheck: A Linux Kernel Module to Verify Temporal Properties of a Task Schedule. In 36th Euromicro Conference on Real-Time Systems (ECRTS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 298, pp. 2:1-2:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{castrovilli_et_al:LIPIcs.ECRTS.2024.2,
  author =	{Castrovilli, Michele and Bini, Enrico},
  title =	{{SlackCheck: A Linux Kernel Module to Verify Temporal Properties of a Task Schedule}},
  booktitle =	{36th Euromicro Conference on Real-Time Systems (ECRTS 2024)},
  pages =	{2:1--2:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-324-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{298},
  editor =	{Pellizzoni, Rodolfo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2024.2},
  URN =		{urn:nbn:de:0030-drops-203054},
  doi =		{10.4230/LIPIcs.ECRTS.2024.2},
  annote =	{Keywords: Linux scheduler, Runtime verification, bounded-delay resource partition, supply function, service curve, real-time calculus, network calculus}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.20
On the Monitorability of Session Types, in Theory and Practice

Authors: Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Software components are expected to communicate according to predetermined protocols and APIs. Numerous methods have been proposed to check the correctness of communicating systems against such protocols/APIs. Session types are one such method, used both for static type-checking as well as for run-time monitoring. This work takes a fresh look at the run-time verification of communicating systems using session types, in theory and in practice. On the theoretical side, we develop a formal model of session-monitored processes. We then use this model to formulate and prove new results on the monitorability of session types, defined in terms of soundness (i.e., whether monitors only flag ill-typed processes) and completeness (i.e., whether all ill-typed processes can be flagged by a monitor). On the practical side, we show that our monitoring theory is indeed realisable: we instantiate our formal model as a Scala toolkit (called STMonitor) for the automatic generation of session monitors. These executable monitors can be used as proxies to instrument communication across black-box processes written in any programming language. Finally, we evaluate the viability of our approach through a series of benchmarks.
Cite as

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 20:1-20:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bartoloburlo_et_al:LIPIcs.ECOOP.2021.20,
  author =	{Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
  title =	{{On the Monitorability of Session Types, in Theory and Practice}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{20:1--20:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.20},
  URN =		{urn:nbn:de:0030-drops-140630},
  doi =		{10.4230/LIPIcs.ECOOP.2021.20},
  annote =	{Keywords: Session types, monitorability, monitor correctness, Scala}
}
Document
Artifact
DOI: 10.4230/DARTS.7.2.2
On the Monitorability of Session Types, in Theory and Practice (Artifact)

Authors: Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
In the paper "On the Monitorability of Session Types, in Theory and Practice" we study the monitorability of message-passing black-box processes against protocol specifications expressed as session types; we formalise a monitor synthesis procedure, prove its correctness, and discuss its implementation - as a tool that synthesises an executable monitor (in the Scala programming language) from a given session type. This artifact contains the aforementioned monitor synthesis tool, called STMonitor; it includes the tool source code, and documentation to reproduce the examples and benchmarks described in the paper.
Cite as

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{bartoloburlo_et_al:DARTS.7.2.2,
  author =	{Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
  title =	{{On the Monitorability of Session Types, in Theory and Practice (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.2.2},
  URN =		{urn:nbn:de:0030-drops-140267},
  doi =		{10.4230/DARTS.7.2.2},
  annote =	{Keywords: Session types, monitorability, monitor correctness, Scala}
}
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.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.8
Consistently-Detecting Monitors

Authors: Adrian Francalanza

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

Abstract
We study a contextual definition for deterministic monitoring based on consistent detections. It is defined in terms of the observed behaviour of the monitor when instrumented over arbitrary systems. We give an alternative, coinductive definition based on controllability which does not rely on system quantifications, and show that it is fully-abstract with respect to the former definition. We then develop a symbolic counterpart to the controllability definition to facilitate an automated analysis for controllable monitors involving data.
Cite as

Adrian Francalanza. Consistently-Detecting Monitors. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{francalanza:LIPIcs.CONCUR.2017.8,
  author =	{Francalanza, Adrian},
  title =	{{Consistently-Detecting Monitors}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{8:1--8:19},
  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.8},
  URN =		{urn:nbn:de:0030-drops-77722},
  doi =		{10.4230/LIPIcs.CONCUR.2017.8},
  annote =	{Keywords: Runtime Monitoring, Deterministic Behaviour, Controllability, Compositional Reasoning, Symbolic Analysis}
}
Document
DOI: 10.4230/DagSemProc.08061.3
A Unified Framework for Verification Techniques for Object Invariants

Authors: Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)

Abstract
Object invariants define the consistency of objects. They have subtle semantics, mainly because of call-backs, multi-object invariants, and subclassing. Several verification techniques for object invariants have been proposed. It is difficult to compare these techniques, and to ascertain their soundness, because of their differences in restrictions on programs and invariants, in the use of advanced type systems (e.g., ownership types), in the meaning of invariants, and in proof obligations. We develop a unified framework for such techniques. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters which guarantee soundness. We instantiate our framework with three verification techniques from the literature, and use it to assess soundness and compare expressiveness.
Cite as

Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers. A Unified Framework for Verification Techniques for Object Invariants. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{drossopoulou_et_al:DagSemProc.08061.3,
  author =	{Drossopoulou, Sophia and Francalanza, Adrian and M\"{u}ller, P. and Summers, Alexander J.},
  title =	{{A Unified Framework for  Verification Techniques for Object Invariants}},
  booktitle =	{Types, Logics and Semantics for State},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8061},
  editor =	{Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.3},
  URN =		{urn:nbn:de:0030-drops-14278},
  doi =		{10.4230/DagSemProc.08061.3},
  annote =	{Keywords: Object invariants, visible states semantics, verification, sound}
}
  • Refine by Author
  • 10 Francalanza, Adrian
  • 6 Aceto, Luca
  • 5 Ingólfsdóttir, Anna
  • 3 Achilleos, Antonis
  • 2 Attard, Duncan Paul
  • Show More...

  • Refine by Classification
  • 4 Software and its engineering → Software verification and validation
  • 2 Software and its engineering → Development frameworks and environments
  • 2 Software and its engineering → Dynamic analysis
  • 2 Theory of computation → Concurrency
  • 2 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 3 monitorability
  • 2 Runtime Verification
  • 2 Runtime instrumentation
  • 2 Scala
  • 2 Session types
  • Show More...

  • Refine by Type
  • 13 document

  • Refine by Publication Year
  • 6 2024
  • 3 2021
  • 2 2018
  • 1 2008
  • 1 2017

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