Quantified Event Automata (QEA) is a specification formalism developed for runtime monitoring. This project is a reimplementation and extension of QEA monitoring techniques (explored in Giles Reger’s PhD work) by Master’s student Helena Cuenca.
The project is still in the development phase. For any queries contact Giles on [email protected].
At the moment we assume the reader is familiar with runtime monitoring concepts. Instructions for the less experienced user will appear later.
See also here for related papers and here for Giles’ thesis. For the RV competition mentioned see here.
For a complete example of how to monitor a property offline see here and for a complete example of how to monitor a property online see here.
These two examples are a good place to start when using the tool for the first time.
We provide a builder to construct QEA’s, found in qea.creation.QEABuilder. In the future we plan to include an external language and a parser that uses this builder.
We will use the canonical HasNext property as an example throughout this text. This is how you could specify this property.
import qea.creation.QEABuilder;
import qea.structure.intf.QEA;
import static qea.structure.impl.other.Quantification.FORALL;
public class Main {
public void main(String[] args) {
QEABuilder builder = new QEABuilder("HasNext");
int i = -1;
builder.addQuantification(FORALL, i);
int HASNEXT_TRUE = 1;
int HASNEXT_FALSE = 2;
int NEXT = 3;
builder.addTransition(1, HASNEXT_TRUE, i, 2);
builder.addTransition(2, HASNEXT_TRUE, i, 2);
builder.addTransition(2, NEXT, i, 1);
builder.addTransition(2, HASNEXT_FALSE, i, 3);
builder.addTransition(3, HASNEXT_FALSE, i, 3);
builder.addFinalStates(1, 2, 3);
QEA qea = builder.make();
}
}If you didn’t want to have to create separate events for true and false return values with hasNext you could also write
import qea.creation.QEABuilder;
import qea.structure.intf.QEA;
import static qea.structure.impl.other.Quantification.FORALL;
import qea.structure.intf.Guard;
public class Main {
public void main(String[] args) {
QEABuilder builder = new QEABuilder("HasNext");
int i = -1;
int b = 1;
builder.addQuantification(FORALL, i);
int HASNEXT = 1;
int NEXT = 2;
builder.addTransition(1, HASNEXT, new int[]{i, b}, Guard.isTrue(b), 2);
builder.addTransition(2, HASNEXT, new int[]{i, b}, Guard.isTrue(b), 2);
builder.addTransition(2, NEXT, i, 1);
builder.addTransition(1, HASNEXT, new int[]{i, b}, Guard.not(Guard.isTrue(b)), 3);
builder.addTransition(3, HASNEXT, new int[]{i, b}, Guard.not(Guard.isTrue(b)), 3);
builder.addFinalStates(1, 2, 3);
QEA qea = builder.make();
}
}However, in general the more features that you use in the specification, the more complex monitoring is. We therefore usually aim to use the simplest features in specification. Future work will look at automated methods for simplification (wrt features).
There are lots of other things we can do when creating QEAs. For more examples see the qeaProperties project. Note that by default states have a next semantics. To make a state a skip state you need to include setSkipStates(state,…).
Creating a monitor is straightforward using qea.monitoring.impl.MonitorFactory:
MonitorFactory.create(qea)
MonitorFactory.create(qea, RestartMode.IGNORE, GarbageMode.LAZY);You can either create a basic monitor or add restart and garbage modes - these are still experimental features but are usually required for pragmatic monitoring.
The restart mode tells the monitor what to do if an ultimate verdict is reached (i.e. violation of a universally quantified property). The choices are
- REMOVE - remove the offending binding
- ROLLBACK - reset the offending binding to the initial state
- IGNORE - reset and ignore this binding in the future
The garbage mode makes certain data structures use weak references - which is only relevant for Online monitoring. The choices are:
- LAZY - what javamop does i.e. use weak maps and clear null references before expanding
- EAGER - monitor garbage collections and actively remove from structures
- UNSAFE_LAZY - the same as lazy but don’t carry out checks to make sure the binding won’t be necessary in the future
To use a monitor you just need to submit an event name and some parameters, for example
monitor.step(HASNEXT, iterator, return_value);
we don’t currently do number of argument of type checks and using events not in the alphabet is invalid.
We assume in online monitoring instrumentation is achieved using AspectJ. We don’t produce aspects automatically. The following is an example of an aspect that would monitor the HasNext property. Scoping might be required on pointcuts depending on exact usage.
package qea;
import java.util.Iterator;
//Imports for QEA
import static qea.structure.impl.other.Quantification.FORALL;
import qea.structure.intf.QEA;
import qea.creation.QEABuilder;
import qea.monitoring.impl.*;
import qea.monitoring.intf.*;
import qea.structure.impl.other.Verdict;
public aspect HasNextAspect {
// Declaring the events
private final int HASNEXT_TRUE = 1;
private final int HASNEXT_FALSE = 2;
private final int NEXT = 3;
//The monitor
Monitor monitor;
// Required if multithreaded as monitor not thread-safe
private Object LOCK = new Object();
pointcut hasNext(Iterator i) : call(* java.util.Iterator+.hasNext()) && target(i);
pointcut next(Iterator i) : call(* java.util.Iterator+.next()) && target(i);
after(Iterator i) returning(boolean b): hasNext(i) {
synchronized(LOCK){
if (b) { check(monitor.step(HASNEXT_TRUE, i)); }
else { check(monitor.step(HASNEXT_FALSE, i)); }
}
}
before(Iterator i) : next(i) {
synchronized(LOCK) {
check(monitor.step(NEXT, i));
}
}
private static void check(Verdict verdict) {
if (verdict == Verdict.FAILURE) {
// Put match detection code here
}
}
public HasNextAspect() {
QEA qea = qea.properties.papers.HasNextQEA;
monitor = MonitorFactory.create(qea);
}
}Note that event names (integers) used here need to match with those used in the QEA.
The normal commands would be required to compile and run with Aspectj - make sure qea-1.0.jar is on the classpath (and qeaProperties if you use those).
It is common to use the DaCapo benchmarks for benchmarking in runtime monitoring. A useful framework has been built for load-time weaving and benchmarking with DaCapo. We have extended this so that QEA can be used in this fork.
The benchmark project contains everything required to perform the benchmarking needed in the OFFLINE track of the RV14 monitoring competition, and other stuff useful for benchmarking. In general, to monitor offline you just need to construct a monitor and manually submit events to it. These extra classes allow for parsing of log files as specified in the RV competition guidelines.
In order to monitor a trace file with the QEA offline monitor, run the class benchmark.competition.offline.QEAOfflineMain specifying in the classpath the following jar files (found in /jars):
- qea-1.0.jar
- qeaOfflineMonitor-1.0.jar
- qeaProperties-1.0.jar
The program takes 3 parameters:
- tracePath: Location of the trace file
- propertyName: Name of the property to monitor. For a list of the available properties
- fileFormat (Optional): The possible values are: CSV and XML. Required when the extension of the trace file is not CSV or XML
For example:
java -cp qeaBenchmark-1.0.jar;qea-1.0.jar;qeaProperties-1.0.jar qea.benchmark.competition.offline.QEAOfflineMain ExistsLeader.csv QEA_OFFLINE_ONE
The following properties from the competition are available and related to the numbered properties in the competition:
- SOLOIST_ONE
- SOLOIST_TWO
- SOLOIST_THREE
- SOLOIST_FOUR
- RITHM_ONE
- RITHM_TWO
- RITHM_THREE
- RITHM_FOUR
- RITHM_FIVE
- MONPOLY_ONE
- MONPOLY_TWO
- MONPOLY_THREE
- MONPOLY_FOUR
- MONPOLY_FIVE
- STEPR_ONE
- STEPR_TWO
- STEPR_THREE
- STEPR_FOUR
- QEA_OFFLINE_ONE
- QEA_OFFLINE_TWO
- QEA_OFFLINE_THREE
- QEA_OFFLINE_FOUR
- QEA_OFFLINE_FIVE
The developers are not very experienced with Maven, but you can add QEA to your project using
<dependency>
<groupId>com.github.selig</groupId>
<artifactId>qea</artifactId>
<version>1.0</version>
<scope>compile</scope>
</dependency>This is what we did in our fork of the DaCapo evaluation framework.