Runtime Verification Based on Register Automata

TL;DR

This paper introduces TOPL automata, a novel formalism for runtime verification of systems with unbounded resource generation, capable of expressing properties beyond current methods, and demonstrates its practical application in Java program verification.

Contribution

The paper presents TOPL automata, a new formalism based on register automata, suitable for expressing complex properties in runtime verification, especially for object-oriented programs.

Findings

TOPL automata are as expressive as register automata.

The method can verify properties involving multiple objects and value chaining.

A tool for Java runtime verification using TOPL automata is developed and validated.

Abstract

We propose TOPL automata as a new method for runtime verification of systems with unbounded resource generation. Paradigmatic such systems are object-oriented programs which can dynamically generate an unbounded number of fresh object identities during their execution. Our formalism is based on register automata, a particularly successful approach in automata over infinite alphabets which administers a finite-state machine with boundedly many input-storing registers. We show that TOPL automata are equally expressive to register automata and yet suitable to express properties of programs. Compared to other runtime verification methods, our technique can handle a class of properties beyond the reach of current tools. We show in particular that properties which require value updates are not expressible with current techniques yet are naturally captured by TOPL machines. On the practical side, we present a tool for runtime verification of Java programs via TOPL properties, where the trade-off between the coverage and the overhead of the monitoring system is tunable by means of a number of parameters. We validate our technique by checking properties involving multiple objects and chaining of values on large open source projects.