You are here

Home › Research › Projects ›

jUnitRV—Temporal Assertions for jUnit

jUnitRV is a tool extending the unit testing framework jUnit by runtime verification capabilities. It provides a new annotation @Monitors listing monitors classes that observe test case execution and verify temporal assertions. In this way, jUnit’s concept of assert-based verification is extended towards checking properties of complete execution paths.

Appetizer

Consider the following property you want all your test cases to obey:

Always (modify  ⇒  ¬ disconnect Until committed)

That is, it must always be the case, that whenever the method modify() is invoked, the client does not disconnect until some call to commit() happened and returned successfully. You can check such properties for dedicated tests following three steps:

1. Declare your events

// You are programming against some class or interface
private static String dataService = "myPackage.DataService";

// Is the application using the service correctly? Let's monitor method invocations!
private static Event modify = called ( dataService , "modify");
private static Event committed = returned ( dataService , "commit");
private static Event disconnect = called ( dataService , "disconnect");

2. Define your monitor

// State, how events are supposed to relate in time
private static Monitor commitBeforeDisconnect = new FLTL4Monitor (
    Always ( 
        implies (
            modify,
            Until ( not ( disconnect ) , committed )
        )
    ));

3. Annotate your test

@Test
@Monitors ({"commitBeforeDisconnect"})
public void test1 () {
    // ...
}

Now you can test your program as usual!

Maven

JUnitRV can be added to a project using the following our repository and the following dependencies to the pom.xml:

<repositories>
    <repository>
        <id>isp-public</id>
        <url>http://sourcecode.isp.uni-luebeck.de/nexus/content/repositories/releases/</url>
    </repository>
</repositories>
 
<dependencies>
    <!-- Dependency for JUnitRV -->
    <dependency>
        <scope>test</scope>
        <groupId>de.uni_luebeck.isp.rvtool</groupId>
        <artifactId>JUnitRV</artifactId>
        <version>0.2.2</version>
    </dependency>
 
    <!-- Dependencies for MMT, Internal Solver -->
    <dependency>
        <scope>test</scope>
        <groupId>de.uni_luebeck.isp.rvtool</groupId>
        <artifactId>EQSupport</artifactId>
        <version>0.2.2</version>
    </dependency>
 
    <!-- Dependencies for MMT, Z3 Solver -->
    <dependency>
        <scope>test</scope>
        <groupId>de.uni_luebeck.isp.rvtool</groupId>
        <artifactId>Z3Support</artifactId>
        <version>0.2.2</version>
    </dependency>
 
    <!-- Support for Salt -->
    <dependency>
        <scope>test</scope>
        <groupId>de.uni_luebeck.isp.rvtool</groupId>
        <artifactId>Salt</artifactId>
        <version>0.2.2</version>
    </dependency>
</dependencies>
 
Examples including sources are contained in the complete bundle below or can be downloaded separately from the maven repository:
 

Download

Installation

  • Download and unzip the package.
  • It contains jUnitRV and all its dependencies.
  • jUnit is already included in the jar file
  • Java 21 needs to be installed.

Usage

To run jUnitRV from the command line use:

    java -cp .:jUnitRV.jar org.junit.runner.JUnitCore junitrvexamples.MyDataClientTest

Or on Windows:

    java -cp .;jUnitRV.jar org.junit.runner.JUnitCore junitrvexamples.MyDataClientTest

Note: The AssertionError is thrown since the example test case is intended to fail.

The example is already compiled. To recompile it use:

    javac -classpath jUnitRV.jar junitrvexamples/*.java

If you want to use jUnitRV inside an IDE or a build tool, just make jUnitRV available on the class path as test dependency.

 

jUnitRV - Monitoring Modulo Theories

First-order constraints inside of LTL formulae as described in [DLT14] is supported since version 0.2.

This version also contains the benchmarks presented in the paper.

Contact

If you have further questions, problems using jUnitRV or want to extend jUnitRV in some way and need access to its source code, feel free to contactthoma [at] isp.uni-luebeck.de ( )Daniel Thoma.