Runtime Verification Based on Register Automata
This addresses the problem of runtime verification for systems with unbounded resources, such as object-oriented programs, offering a novel method to express properties involving value updates that current tools cannot handle.
The authors tackled runtime verification of systems with unbounded resource generation, such as object-oriented programs, by proposing TOPL automata based on register automata, showing they can handle properties beyond current tools while maintaining equal expressiveness. They validated their approach with a tool for Java programs, demonstrating tunable trade-offs between coverage and monitoring overhead on large open-source projects.
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.