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.
|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|
|Number of pages||19|
|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
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|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|
|Period||14/06/21 → 18/06/21|
Bibliographical noteFunding 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.
© 2021, IFIP International Federation for Information Processing.