Bidirectional Runtime Enforcement of First-Order Branching-Time Properties

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

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2023-01, Vol.19, Issue 1
Main Authors: Aceto, Luca, Cassar, Ian, Francalanza, Adrian, Ingolfsdottir, Anna
Format: Article
Language:English
Subjects:
computer science - logic in computer science
computer science - programming languages
computer science - software engineering
d.2.4
f.3.1
f.3.2
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1860-5974
1860-5974
DOI:10.46298/lmcs-19(1:14)2023