A Purely Functional Approach to LTL Runtime Verification

A Purely Functional Approach to LTL Runtime Verification

Ettore Speziale
DEI PhD Student

DEI - Sala Seminari
October 7th, 2011
at 5.30 p.m.

Abstract:


Checking a system against a set of properties can be performed by employing a model checker with a model of the system. Usually, model checking requires a considerable amount of resources. A complementary technique, closer to testing, is runtime verification: the system to be checked emits an execution trace that is checked against a set of properties while the system is running. In this work, the execution trace is monitored by means of an alternating Buechi automaton built from the LTL formula describing the properties we want to check.
We show how the runtime model checker has been implemented exploring the pure functional language Haskell, allowing a fast implementation of the automata formal description.

Research Area:
Advanced software architectures and methodologies