Runtime enforcement of reactive systems using synchronous enforcers

Autor:	Pinisetty, Srinivas, Roop, Partha S, Smyth, Steven, Tripakis, Stavros, von Hanxleden, Reinhard
Rok vydání:	2016
Předmět:	Computer Science - Formal Languages and Automata Theory Computer Science - Software Engineering
Druh dokumentu:	Working Paper
Popis:	Synchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem of runtime enforcement in the context of synchronous programs. We propose a framework where an enforcer monitors both the inputs and the outputs of a synchronous program and (minimally) edits erroneous inputs/outputs in order to guarantee that a given property holds. We define enforceability conditions, develop an online enforcement algorithm, and prove its correctness. We also report on an implementation of the algorithm on top of the KIELER framework for the SCCharts synchronous language. Experimental results show that enforcement has minimal execution time overhead, which decreases proportionally with larger benchmarks. Comment: Keywords: Runtime monitoring, Runtime Enforcement, Automata, Safety properties, Synchronous programming, SCCharts synchronous language
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1612.05030 Zobrazit plný text záznamu View this record from Arxiv