MahaRAJA

What is MahaRAJA?

The MahaRAJA framework is an efficient event-based runtime verification software tool for verifying at runtime the relationship among events and their temporal properties on Java programs. Monitoring is achieved through the co-execution of the formal specification and the system under test. The monitor continuously evaluates the conformance of the concrete implementation with respect to its formal specification given in terms of Time Basic Petri nets.

Bibliography

Use the following reference to cite this work:

1. Camilli M., Gargantini A., Scandurra P., Bellettini C. (2017) Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets. In: Barrett C., Davies M., Kahsai T. (eds) NASA Formal Methods. NFM 2017. Lecture Notes in Computer Science, vol 10227. Springer, Cham

Source code

The source code of MahaRAJA is available at https://bitbucket.org/maharajaframework/maharajaframework. The repository contains the main components of the monitoring tool and some examples of monitored Java programs along with associated Time Basic (TB) Petri net models.

MahaRAJA is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. MahaRAJA is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with MahaRAJA. If not, see http://www.gnu.org/licenses/.

Runnable Examples

A simple producer-consumer runnable example is available at monitored-prodcons.jar. To run this example you can type:

java -jar monitored-prodcons.jar -m producer-consumer.xml

You can find the "producer-consumer.xml" model in the resources package of the MahaRAJA project. The monitor logs at runtime the execution of the action methods. If the conformance relationship between the model and the implementation does not hold, the monitor throws an Exception containing some useful information about the failure.

A simple elevator runnable example is available at monitored-elevator.jar. To run this example you can type:

java -jar monitored-elevator.jar -m elevator.xml

You can find the "elevator.xml" model in the resources package of the MahaRAJA project.

The .xml file representing a TB net follows an extended version of the Petri Net Markup Language. To view and edit TB net files you can use a customized version of the PIPE2 editor available at pipe.zip.

Configuration

We ran our experiments on a machine equipped with a (six core) Intel Xeon E5-2630 at 2.30GHz CPU, 32GB of RAM, the Ubuntu 14.04.3 LTS (GNU/Linux 3.13.0-39-generic x86 64) operating system, and the Java HotSpot 1.8 64-Bit Server virtual machine.

The following JVM options were applied to reduce the garbage collector (GC) interference and to avoid full GC runs.

-Xms2g -Xmx2g -XX:ParallelGCThreads=6 -XX:G1HeapRegionSize=4m -XX:+UseG1GC -XX:G1HeapWaste=5 -XX:InitiatingHeapOccupancyPercent=85 -XX:+UnlockExperimentalVMOptions -XX:G1MixedGCLiveThresholdPercent=85

The options reported above are hints and their effectiveness varies depending on the specific hardware/software environment. keep in mind that GC tuning is the last task to be done. The number of objects necessary to be cleared by the garbage collector as well as the number of GCs to be executed depend on the number of objects which have been created. Therefore, to control the GC performed by your system, you should, first, decrease the number of objects created.

If you are not sure how to set the JVM options properly, you can just use the "UseG1GC". In fact, the G1 GC is an adaptive garbage collector with defaults that enable it to work efficiently without modification.

Refer to the official documentation for more information.

Testing

In order to help the user to increase the confidence about the correctness of the SUT, the MahaRAJA software tool can be used in conjunction with JUnit to generate different monitored test cases. This way, the user can integrate our runtime verification technique with assertions on variables and on specific goal conditions, terms of ⟨M, C⟩ pairs, where M represents a reachable marking and C is a temporal constraint (i.e., a set of linear inequalities involving the timestamps of M).

An example of JUnit test case along with a goal condition is reported in the following code snippet.

@Test
public void brakeTest() {
  CruiseControl cc = new CruiseControl();
  Monitor monitor = new Monitor(cc, model);
  monitor.start();
  cc.controllableAction(Action.getAcceleration());
  randomSleep(100, 5000);
  cc.controllableAction(Action.getCruisingOn());
  randomSleep(100,5000);
  cc.controllableAction(Action.brakeOnActReq());
  randomSleep(100, 2000);
  String m="BrakeOn{T1}CruisingOff{T2}EngineOn{T0}";
  String c="T2<=T1+50";
  assertTrue(Monitor.goalReached(m, c));
  monitor.shutDown();
}

This test verifies that the difference between T1 and T2 is less than 50 ms, which represents the expected reaction time to the brake-on signal.

Comparative evaluation

This section reports a preliminary quantitative comparison between MahaRAJA and two other representative state-of-the-art runtime verification software tools, supporting the verification of temporal properties: Larva and Java-Mac. Although, they support different features and have modeling formalisms with different expressiveness, we tried to enable a common ground comparison by using only a common subset of the available features: the verification of temporal properties associated with the initial and final time of a single event repeatedly executed.

In particular the graphs reported below have been generated by running the producer-consumer example and observing ~10⁶ consumption events. All the runs have been performed on the same machine (reported above) with the same JVM (without optimizations), and same workload conditions.

This preliminary quantitative comparison individuates MahaRAJA as the less invasive tool. This means that MahaRAJA is more suitable to monitor highly time sensitive systems.

Downloads

tool	sources/executables	specification	how to
MahaRAJA	MahaRAJA P/C	consume.xml	this webpage
Larva	larva-prodcons.zip	consume.lrv	LARVA webpage
Java-Mac	javamac-prodcons.zip	consume.pedl, consume.medl	Java-Mac webpage