On Bidirectional Runtime Enforcement

Luca Aceto, Ian Cassar, Adrian Francalanza*, Anna Ingólfsdóttir

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.

Original languageEnglish
Title of host publicationFormal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings
EditorsKirstin Peters, Tim A. Willemse
PublisherSpringer Science and Business Media Deutschland GmbH
Pages3-21
Number of pages19
ISBN (Print)9783030780883
DOIs
Publication statusPublished - 2021
Event41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 - Virtual, Online
Duration: 14 Jun 202118 Jun 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12719 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021
CityVirtual, Online
Period14/06/2118/06/21

Bibliographical note

Funding Information:
This work was partly supported by the projects “TheoFoMon: Theoretical Foundations for Monitorability” (nr.163406-051),“Developing Theoretical Foundations for Runtime Enforcement” (nr.184776-051) and “MoVeMnt: Mode(l)s of Verification and Monitorability” (nr.217987-051) of the Icelandic Research Fund, by the Italian MIUR project PRIN 2017FTXR7S IT MATTERS “Methods and Tools for Trustworthy Smart Systems”, by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement nr. 778233, and by the Endeavour Scholarship Scheme (Malta), part-financed by the European Social Fund (ESF) - Operational Programme II – 2014–2020.

Publisher Copyright:
© 2021, IFIP International Federation for Information Processing.

Fingerprint

Dive into the research topics of 'On Bidirectional Runtime Enforcement'. Together they form a unique fingerprint.

Cite this