Bounded Serial Compositional Runtime Enforcement

By: Saumya Shankar, Thierry Jéron, Prisha Srinidi, Srinivas Pinisetty

Abstract

Runtime enforcement is a monitoring technique used to ensure that a system behaves according to a set of formal properties. This paper addresses the enforcement of multiple properties modelled as finite automata, where their enforcers are composed serially to promote modularity. The paper considers enforcers operating with bounded memory and explores whether regular properties and their subclasses can be enforced in the compositional setting under memory constraints, presenting the Bounded Serial Compositional Runtime Enforcement framework with a prototype implementation.

Keywords

Formal verification, Runtime enforcement, Bounded-memory, Serial composition, Regular property, Safety and co-safety property, Automata

Cite as:

Saumya Shankar, Thierry Jéron, Prisha Srinidi, Srinivas Pinisetty, “Bounded Serial Compositional Runtime Enforcement”, Journal of Object Technology, Volume 25, no. 1 ( 2026), pp. 1:1-19, doi:10.5381/jot.2026.25.1.a11.

DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn