.png){kind=icon}
.png){kind=icon}
Return
Bounded Serial Compositional Runtime Enforcement
.png){kind=icon}
PRE
AI
DOI：10.5381/jot.2026.25.1.a11.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Runtime enforcement is a monitoring technique used to ensure that a system behaves according to a set of formal properties. It employs an enforcer that transforms an untrusted sequence of events into one that satisfies the specified property. In cases of property violation, we allow the enforcer to temporarily delay input events (i.e., storing them in memory until the property can be satisfied) or to suppress them if the property can never be satisfied. This paper addresses the enforcement of multiple (untimed) properties modelled as finite automata, where their enforcers are composed serially, to promote modularity, i.e., rather than synthesizing a single enforcer for all properties, we generate individual enforcers and combine them serially. Also, to handle practical constraints, the paper considers that each enforcer operates with bounded (finite) memory. We explore whether regular properties and their subclasses, specifically safety (nothing bad happens) and co-safety (something good eventually happens) can be enforced in the compositional setting under memory constraints. We define enforceability in terms of preserving key criteria like soundness, transparency. For properties that are not inherently serially enforceable, we identify specific conditions on their automata whose satisfaction allows certain groups of properties to become serially enforceable. To formalize and support these ideas, we present the Bounded Serial Compositional Runtime Enforcement framework. We provide a prototype implementation and evaluate the performance of the proposed serial enforcer to demonstrate practical feasibility.
Keywords:
Formal verification
Runtime enforcement
Bounded-memory
Serial composition
Regular property
Safety and co-safety property
Automata
Journal
J
IF:
1.4
Papers:
20
Citations:
0