Talk "Online Monitoring of Distributed Systems with a Five-valued LTL"

by Holger Schlingloff

Fri, 10 January 2014 at 02:30 pm in Theddingworth near Leicester, UK

Joint work with: Chai Ming

Abstract: This talk deals with specification-based monitoring of distributed systems as opposed to verification and testing. In this realm, we show how to deal with two kinds of uncertainties. On one hand, the order of causally unrelated executions is not determined because we cannot assume that there exists a global clock. On the other hand, in a finite amount of time, the behaviour can be observed only up to a certain moment, and the future behaviour is unknown. In the presentation, we investigate a monitoring approach based on linear temporal logic (LTL) specifications. We propose a five-valued semantics for LTL to deal with both kinds of uncertainties. We develop an efficient runtime verification algorithm using formula rewriting, and show the feasibility of our approach with a case study in the railway domain.