Runtime verification of LTL and TLTL

Abstract

In a nutshell, runtime verification comprises methods that help in establishing whether or not the actual behaviour of a running system complies with the expected behaviour. Runtime verification of LTL and TLTL employ temporal logic to specify the expected behaviour formally, and derive the so-called monitors automatically. Application areas include safety and security critical systems, where additional checks are required to ensure that systems don't reach a failure state that may otherwise have dire consequences for its users and/or the environment. This talk will first introduce the general ideas behind runtime verification, and then explain how efficient monitors can be generated from LTL specifications. We discuss the complexity of the presented monitor generation algorithm, and give some experimental results from an accompanying implementation. The second part of the talk concerns real-time systems, where the expected behaviour cannot be described by LTL anymore, instead it is described in a dedicated real-time logic, TLTL (aka state clock logic). Given a TLTL formula, we then show how to generate the corresponding monitors from it, which can be used to observe the behaviour of real-time systems, and raise alarms if behavioural aberrations occur.

Biography

Andreas Bauer is currently a Senior Research Engineer at National ICT Australia (NICTA), and an adjunct Research Fellow at the Australian National University. Prior to working at NICTA, he was a full-time Research Fellow in the Logic and Computation group of the Australian National University (2007-2009). Andreas obtained his PhD from the Technische University Munich, Germany, where he worked as a Research Assistant in Prof. Bory's Software and Systems Engineering group (2003-2007). His thesis was on a temporal logic based framework for monitoring and diagnosing distributed reactive systems. For more information, visit his homepage.