Runtime Enforcement for Component-Based Systems

The paper Runtime Enforcement for Component-Based Systems has been accepted for publication in SAC-SVT 2015, the 30th ACM/SIGAPP Symposium On Applied Computing – Software Verification and Testing track, Salamanca, Spain.

Here is the abstract of the paper.

We propose a theoretical runtime enforcement framework for component-based systems (CBS) where we delineate a hierarchy of enforceable properties (i.e., properties that can be enforced) according to the number of observational steps a system is allowed to deviate from the property (i.e., the notion of k-step enforceability). To ensure the observational equivalence between the correct executions of the initial system and the monitored system, we show that i) only stutter-invariant properties should be enforced on CBS with our monitors, ii) safety properties are 1-step enforceable. Given an abstract enforcement monitor for some 1-step enforceable property, we formally instrument (at relevant locations) a system to integrate the monitor. At runtime, the monitor observes and automatically avoids any error in the behavior of the system w.r.t. the property.

This is joint work with H. Charafedine, K. El-Harake, and M. Jaber.