This paper considers a generic approach to enhance traditional runtime verification techniques towards first-order theories in order to reason about data. This allows especially for the verification of multi-threaded, object-oriented systems. It presents a general framework lifting the monitor synthesis for propositional temporal logics to a temporal logic over structures within some first-order theory. To evaluate such temporal properties, SMT solving and classical monitoring of propositional temporal properties is combined. The monitoring procedure was implemented for linear-time temporal logic (LTL) based on the Z3 SMT solver and evaluated regarding runtime performance.
|Title of host publication||Tools and Algorithms for the Construction and Analysis of Systems|
|Number of pages||16|
|Place of Publication||Berlin|
|Publication status||Published - 01.04.2014|
|Event||20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Grenoble, France|
Duration: 05.04.2014 → 13.04.2014
Conference number: 105112