2008 | OriginalPaper | Buchkapitel
Impartial Anticipation in Runtime-Verification
verfasst von : Wei Dong, Martin Leucker, Christian Schallhart
Erschienen in: Automated Technology for Verification and Analysis
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
μ
-calculus,
PLTL
mod
,
SiS
, and
RLTL
.