Specification and optimal reactive synthesis of run-time enforcement shields

A run time enforcement shield is a controller which corrects the output O of a system with sporadic errors (SSE) so as to guarantee the invariance of a critical requirement. Moreover, the shield output O′ must deviate from the SSE output O “as little as possible” to maintain the quality. We give a method for logical specification of shields using logic QDDC. The specification consists of a correctness requirement REQ, a mandatory hard deviation constraint HDC, and a soft deviation constraint SDC whose satisfaction must be optimized in an H-optimal fashion. We show how a tool DCSynth implementing soft requirement guided synthesis is used for the automatic synthesis of shields from such specifications. Next, we give logical formulation of various notions of shields including Bloem's k-Stabilizing shield, Wu's Burst-error shield, as well as new EK-shield and Windowed-EK-shield. We experimentally compare the performance of the shields synthesized under these notions.