Abstract
We introduce a formal framework to provide an efficient event-based monitoring technique, and we describe its current implementation
as the MahaRAJA software tool. The framework enables the quantitative runtime verification of temporal properties extracted
from occurring events on Java programs. The monitor continuously evaluates the conformance of the concrete implementation
with respect to its formal specification given in terms of Time Basic Petri nets, a particular timed extension of Petri nets.
The system under test is instrumented by using simple Java annotations on methods to link the implementation to its formal
model. This allows a separation between implementation and specification that can be used for other purposes such as formal
verification, simulation, and model-based testing. The tool has been successfully used to monitor at runtime and test a number
of benchmarking case-studies. Experiments show that our approach introduces bounded overhead and effectively reduces the involvement
of the monitor at run time by using negligible auxiliary memory. A comparison with a number of state-of-the-art runtime verification
tools is also presented.
[download the pdf file] [DOI]