Monitoring of Real-Time Properties

11 years 5 months ago
Monitoring of Real-Time Properties
This paper presents a construction for runtime monitors that check real-time properties expressed in timed LTL (TLTL). Due to D'Souza's results, TLTL can be considered a natural extension of LTL towards real-time. Moreover, a typical obstacle in runtime verification is solved both for untimed and timed formulae, in that standard models of linear temporal logic are infinite traces, whereas in runtime verification only finite system behaviours are at hand. Therefore, a 3valued semantics (true, false, inconclusive) for LTL and TLTL on finite traces is defined that resembles the infinite trace semantics in a suitable and intuitive manner. Then, the paper describes how to construct, given a (T)LTL formula, a deterministic monitor with three output symbols that reads a finite trace and yields its according 3-valued (T)LTL semantics. Notably, the monitor rejects a trace as early as possible, in that any minimal bad prefix results in false as a return value.
Andreas Bauer 0002, Martin Leucker, Christian Scha
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2006
Authors Andreas Bauer 0002, Martin Leucker, Christian Schallhart
Comments (0)