Mufin–Runtime Monitoring with Union-Find Structures

Mufin is a tool for runtime verification of object-oriented software system. It uses a novel algorithm for monitoring the individual behaviour and interaction of an unbounded number of runtime objects. This allows for evaluating complex correctness properties that take runtime data in terms of object identities into account. In particular, the underlying formal model can express hierarchical interdependencies of individual objects. Currently, the most efficient monitoring approaches for such properties are based on lookup tables. In contrast, the proposed algorithm uses union-find data structures to manage individual instances and thereby accomplishes a significant performance improvement. The time complexity bounds of the very efficient operations on union-find structures transfer to our monitoring algorithm: the execution time of a single monitoring step is guaranteed logarithmic in the number of observed objects. The amortised time is bound by an inverse of Ackermann’s function. Benchmarks show that the targeted class of properties can be monitored extremely efficient and runtime overhead is reduced substantially compared to other tools.

Publication

The details of the implemented algorithm are described in

• Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz, Daniel Thoma: Runtime Monitoring with Union-Find Structures. In Marsha Chechik, Jean-François Raskin (Eds.): International Conference on Tools and Algorithms for the Construction and Analysis of Systems, International Conference, TACAS 2016, LNCS 9636, Springer (2016).

See also the presentation slides for TACAS 2016.

Benchmarks and Usage Example

The tool binary and benchmark examples are available for download at the following location.

• Mufin Benchmark Package

The archive contains the benchmarks used to compare the performance of Mufin with the tools JavaMOP and MarQ. Details are described in the related paper "Runtime Monitoring with Union-Find Structures" (see above). The benchmarks and property specifications are adopted from the 2nd Competition on Runtime Verification (CRV’15).

The archive contains the source code of the benchmarks and the property specifications for use with Mufin and Mufin weak. The monitoring tools are packaged in a way that only Java 8 is required to run the benchmarks. All other dependencies are included (Copyright remains with the respective holders.) The folder `benchmarks` contains the source code of the benchmarks. Each benchmark can be compiled using the `build.sh` shell script, which creates executable jar files. These jar files can be executed to measure a performance baseline of the non-instrumented case.

The folder `monitors` contains the source code for the property specification and the instrumentation done with the two tools. Each folder contains a shell script `build.sh` to compile the code and another shell script `run.sh` to execute it. One needs to build the benchmark first. Mufin uses the JVM contained in the folder `openjdk`, which is compiled for Linux 64 Bit systems and contains a custom patch needed for instrumenting the base Object class. Mufin weak avoids the need for this patch by using a hash table data structure on the first level.

People

Mufin was developed by

• Normann Decker,
• Jannis Harder,
• Torben Scheffel,
• Malte Schmitz, and
• Daniel Thoma.

For more information feel free to contact them.

Acknowledgements

•   The project Mufin was undertaken partly in the scope of our engagement in the project CONIRAS.
• The work was partially supported by the European Cooperation in Science and Technology (COST Action ARVI)