Bidirectional Runtime Enforcement of First-Order Branching-Time Properties

TL;DR

This paper introduces a novel bidirectional runtime enforcement framework for system properties, specifically focusing on the safety fragment of sHML, and provides automated monitor synthesis ensuring correctness.

Contribution

It develops an operational framework for bidirectional enforcement and automates monitor synthesis from sHML formulas, demonstrating enforceability of these properties.

Findings

Automated synthesis of correct monitors from sHML formulas.

Bidirectional enforcement monitors can enforce safety properties.

The enforceability of sHML safety fragment via action disabling monitors.

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.