Runtime enforcement of reactive systems using synchronous enforcers

TL;DR

This paper introduces a framework for runtime enforcement in synchronous reactive systems, where an enforcer monitors and minimally edits inputs and outputs to ensure property compliance with minimal overhead.

Contribution

It proposes a novel enforcement framework with enforceability conditions, an online algorithm, and an implementation demonstrating minimal overhead in synchronous programs.

Findings

Enforcement ensures property satisfaction with minimal runtime overhead.

The online enforcement algorithm is proven correct.

Implementation on KIELER framework shows scalable performance.

Abstract

Synchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem of runtime enforcement in the context of synchronous programs. We propose a framework where an enforcer monitors both the inputs and the outputs of a synchronous program and (minimally) edits erroneous inputs/outputs in order to guarantee that a given property holds. We define enforceability conditions, develop an online enforcement algorithm, and prove its correctness. We also report on an implementation of the algorithm on top of the KIELER framework for the SCCharts synchronous language. Experimental results show that enforcement has minimal execution time overhead, which decreases proportionally with larger benchmarks.