author = {Wolfgang Schreiner and Temur Kutsia},
title = {{A Resource Analysis for LogicGuard Monitors}},
language = {english},
abstract = {We describe a static analysis that we have devised to determine whether a specification expressed in the LogicGuard language gives rise to a monitor that can operate with a finite amount of resources, notably with finite histories of the streams that are monitored. This information can be passed to the runtime system of the monitor such that after every execution step the histories of the monitored streams can be appropriately pruned and the monitor can operate for an indefinite amount of time with a limited amount of memory. First, the analysis is presented for an abstract core language that monitors a single stream; the soundness of the analysis with respect to a formal operational semantics is verified in a companion paper. Second, we extend the analysis to an extended version of the language that can monitor multiple streams and supports the construction of virtual streams. This version already resembles the concrete LogicGuard language that is supported by the current prototype implementation. For the purpose of the analysis, several features of the language differ between the abstract and the concrete form; before the analysis can be implemented, the concrete language has to be correspondingly revised.},
year = {2013},
month = {December 17},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, runtime verification, predicate logic},
sponsor = {FFG BRIDGE Project 832207 "LogicGuard"},
length = {45}