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 |
|---|---|
| Pages (from-to) | 14:1-14:44 |
| Journal | Logical Methods in Computer Science |
| Volume | 19 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 28 Feb 2023 |
Bibliographical note
Funding Information:Key words and phrases: runtime monitors, property enforcement, monitor synthesis, first-order safety properties, modal µ-calculus. “TheoFoMon: Theoretical Foundations for Monitorability” (nr.163406-051) and “MoVeMnt: Mode(l)s of Verification and Monitorability” (nr.217987-051) of the Icelandic Research Fund, the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement nr. 778233, the Italian MIUR project PRIN 2017FTXR7S IT MATTERS “Methods and Tools for Trustworthy Smart Systems”, the Research Excellence Funds of the University of Malta, 2021 nr. I22LU01, and the Endeavour Scholarship Scheme (Malta), part-financed by the European Social Fund (ESF) - Operational Programme II – 2014-2020.
Publisher Copyright:
© L. Aceto, I. Cassar, A. Francalanza, and A. Ingólfsdóttir ○CC Creative Commons.
Other keywords
- first-order safety properties
- modal µ-calculus
- monitor synthesis
- property enforcement
- runtime monitors