Runtime Verification on Abstract Finite State Models

TL;DR

This work presents JIV$^2$E, a runtime verification framework that extracts abstract finite-state models from Java program executions and performs online property checking on property-preserving abstractions. It distinguishes data-oriented and control-oriented models, using boolean and multi-valued abstractions or path-based abstractions to keep models tractable for long runs. A dedicated property specification language with $F$, $G$, and $P$ operators, along with iteration and datatype support, enables expressive verification over finite traces. The approach is demonstrated on case studies such as a Multirotor Drone Controller, OAuth 2.0 protocol, and Apache Tomcat, showing substantial reductions in state space and verification time while enabling online verification with targeted event collection. The work highlights practical trade-offs between abstraction granularity and verification guarantees, and points to future work on broader language support, improved visualization, and distributed monitoring.

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.

Figures (7)

• Figure 1: Abstractions for data-oriented models.
• Figure 2: Sample abstractions for control-oriented models
• Figure 3: Screenshot of JIV$^2$E for off-line property-checking on a runtime abstract model of the Dining Philosophers program execution. The boolean abstraction function is: p$_i$== E, for $i=1..5$. All 11 abstract states are shown in the figure. Each state component is abbreviated by the value E or $\sim$ E, where the latter abstracts the concrete values T and H. The green-highlighted state is the start state.
• Figure 4: Property Checking on Abstract State Models with Multi-valued Abstractions
• Figure 5: The JIV$^2$E Online Verification Architecture with Byte-Code Instrumentation. The User Interface shows the abstract state diagram for an erroneous run of the Dining Philosophers problem. The property checker highlights in red the erroneous state as it occurred.

Theorems & Definitions (7)

• definition 1
• definition 2
• definition 3
• definition 4
• definition 5
• definition 6
• definition 7