Event-based runtime verification of temporal properties using time basic Petri nets

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.