Specification and Optimal Reactive Synthesis of Run-time Enforcement Shields

Paritosh K. Pandya
(Tata Institute of Fundamental Research, Mumbai)
Amol Wakankar
(Homi Bhabha National Institute, Mumbai and Bhabha Atomic Research Centre, Mumbai)

A system with sporadic errors (SSE) is a controller which produces high quality output but it may occasionally violate a critical requirement REQ(I,O). A run-time enforcement shield is a controller which takes (I,O) (coming from SSE) as its input, and it produces a corrected output O' which guarantees the invariance of requirement REQ(I,O'). Moreover, the output sequence O' must deviate from O "as little as possible" to maintain the quality. In this paper, we give a method for logical specification of shields using formulas of logic Quantified Discrete Duration Calculus (QDDC). The specification consists of a correctness requirement REQ as well as a hard deviation constraint HDC which must both be mandatorily and invariantly satisfied by the shield. Moreover, we also use quantitative optimization to give a shield which minimizes the expected value of cumulative deviation in an H-optimal fashion. We show how tool DCSynth implementing soft requirement guided synthesis can be used for automatic synthesis of shields from a given specification. Next, we give logical formulas specifying several notions of shields including the k-Stabilizing shield of Bloem "et al." as well as the Burst-error shield of Wu "et al.", and a new e,d-shield. Shields can be automatically synthesized for all these specifications using the tool DCSynth. We give experimental results showing the performance of our shield synthesis tool in relation to previous work. We also compare the performance of the shields synthesized under diverse hard deviation constraints in terms of their expected deviation and the worst case burst-deviation latency.

In Jérôme Leroux and Jean-Francois Raskin: Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2019), Bordeaux, France, 2-3rd September 2019, Electronic Proceedings in Theoretical Computer Science 305, pp. 91–106.
Published: 18th September 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.305.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org