On Bidirectional Runtime Enforcement

Luca Aceto; Ian Cassar; Adrian Francalanza; Anna Ingólfsdóttir

doi:10.1007/978-3-030-78089-0_1

On Bidirectional Runtime Enforcement

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

^*Corresponding author for this work

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-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 language	English
Title of host publication	Formal 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
Editors	Kirstin Peters, Tim A. Willemse
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	3-21
Number of pages	19
ISBN (Print)	9783030780883
DOIs	https://doi.org/10.1007/978-3-030-78089-0_1
Publication status	Published - 2021
Event	41st 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 2021 → 18 Jun 2021

Publication series

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

Conference

Conference	41st 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
City	Virtual, Online
Period	14/06/21 → 18/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.

Access to Document

10.1007/978-3-030-78089-0_1

Cite this

Aceto, L., Cassar, I., Francalanza, A., & Ingólfsdóttir, A. (2021). On Bidirectional Runtime Enforcement. In K. Peters, & T. A. Willemse (Eds.), Formal 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 (pp. 3-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12719 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-78089-0_1

Aceto, Luca ; Cassar, Ian ; Francalanza, Adrian et al. / On Bidirectional Runtime Enforcement. Formal 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. editor / Kirstin Peters ; Tim A. Willemse. Springer Science and Business Media Deutschland GmbH, 2021. pp. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{8a4ab10dea134870bad5bae4efc6dbe5,

title = "On Bidirectional Runtime Enforcement",

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.",

author = "Luca Aceto and Ian Cassar and Adrian Francalanza and Anna Ing{\'o}lfsd{\'o}ttir",

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: {\textcopyright} 2021, IFIP International Federation for Information Processing.; 41st 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 ; Conference date: 14-06-2021 Through 18-06-2021",

year = "2021",

doi = "10.1007/978-3-030-78089-0_1",

language = "English",

isbn = "9783030780883",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "3--21",

editor = "Kirstin Peters and Willemse, {Tim A.}",

booktitle = "Formal 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",

address = "Germany",

}

Aceto, L, Cassar, I, Francalanza, A & Ingólfsdóttir, A 2021, On Bidirectional Runtime Enforcement. in K Peters & TA Willemse (eds), Formal 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12719 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 3-21, 41st 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, 14/06/21. https://doi.org/10.1007/978-3-030-78089-0_1

On Bidirectional Runtime Enforcement. / Aceto, Luca; Cassar, Ian; Francalanza, Adrian et al.

Formal 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. ed. / Kirstin Peters; Tim A. Willemse. Springer Science and Business Media Deutschland GmbH, 2021. p. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12719 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - On Bidirectional Runtime Enforcement

AU - Aceto, Luca

AU - Cassar, Ian

AU - Francalanza, Adrian

AU - Ingólfsdóttir, Anna

N1 - 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.

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85111359601&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-78089-0_1

DO - 10.1007/978-3-030-78089-0_1

M3 - Conference contribution

AN - SCOPUS:85111359601

SN - 9783030780883

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 21

BT - Formal 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

A2 - Peters, Kirstin

A2 - Willemse, Tim A.

PB - Springer Science and Business Media Deutschland GmbH

T2 - 41st 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

Y2 - 14 June 2021 through 18 June 2021

ER -

Aceto L, Cassar I, Francalanza A, Ingólfsdóttir A. On Bidirectional Runtime Enforcement. In Peters K, Willemse TA, editors, Formal 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. Springer Science and Business Media Deutschland GmbH. 2021. p. 3-21. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-78089-0_1

On Bidirectional Runtime Enforcement

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this