Runtime Verification on Abstract Finite State Models

TL;DR

This paper presents a method for extracting and verifying finite state models from multi-threaded Java programs at runtime, using property-preserving abstractions to enable efficient online correctness checks.

Contribution

It introduces a technique for constructing reduced, abstract models from program runs that preserve properties, facilitating efficient runtime verification of complex concurrent systems.

Findings

Effective abstraction functions enable property preservation.

Online verification reduces runtime overhead.

Case studies demonstrate practical applicability.

Abstract

Finite-state models are ubiquitous in the study of concurrent systems, especially controllers and servers that operate in a repetitive cycle. In this paper, we show how to extract finite state models from a run of a multi-threaded Java program and carry out runtime verification of correctness properties. These properties include data-oriented and control-oriented properties; the former express correctness conditions over the data fields of objects, while the latter are concerned with the correct flow of control among the modules of larger software. As the extracted models can become very large for long runs, the focus of this paper is on constructing reduced models with user-defined abstraction functions that map a larger domain space to a smaller one. The abstraction functions should be chosen so that the resulting model is property preserving, i.e., proving a property on the abstract model carries over to the concrete model. The main contribution of this paper is in showing how runtime verification can be made efficient through online property checking on property-preserving abstract models. The property specification language resembles a propositional linear temporal logic augmented with simple datatypes and operators. Classic concurrency examples and larger case studies (Multi-rotor Drone Controller, OAuth Protocol) are presented in order to demonstrate the usefulness of our proposed techniques, which are incorporated in an Eclipse plug-in for runtime visualization and verification of Java programs.