Impartial Anticipation in Runtime-Verification

In this paper, a uniform approach for synthesizing monitors checking correctness properties specified in linear-time logics at runtime is provided. Therefore, a generic three-valued semantics is introduced reflecting the idea that prefixes of infinite computations are checked. Then a conceptual framework to synthesize monitors from a logical specification to check an execution incrementally is established, with special focus on resorting to the automata-theoretic approach. The merits of the presented framework are shown by providing monitor synthesis approaches for a variety of different logics such as LTL, the linear-time

• Type: Conference
• Year: 2008
• Where: ATVA
• Authors: Wei Dong, Martin Leucker, Christian Schallhart
• Keywords: ATVA 2008, Generic Three-valued Semantics, Hardware, Linear-time Logics, Monitors Checking Correctness