LTL-FO+ Runtime Monitoring

This form takes an input specification and generates an AspectJ file that monitors that specification. Please read the demo if you don't know what to do.

Enter your specification here.

Input language reference

A typical specification file is as follows:

PROTOTYPES
int methodName1(int p1, String p2);
int methodName2(int p3);
...

SPEC LTL-FO+
G ([m1 /call/method] (
  [v1 /params/p1] (((x) = ({methodName1})) -> (
    X (G ([m2 /call/method] ([v2 /params/p3] (
      ((m2) = ({methodName2})) -> (!((v1) = (v2)))))))))))


@FALSE {
  // Some Java code
}

@TRUE {
  // Some Java code
}

@INCONCLUSIVE {
  // Some Java code
}

In the PROTOTYPES section, you declare the method prototypes you want to be processed by the monitor. The only method calls that will be processed are those defined here. These prototypes are also used to refer to method arguments by their names in the LTL-FO+ formula below; for example, the second argument of the method methodName1(int, String) is called p2.

In the SPEC LTL-FO+ section, you specify exactly one LTL-FO+ formula. See the syntax and semantics of LTL-FO+ for help.

In the @TRUE, @FALSE and @INCONCLUSIVE sections, you write Java code you want to be executed when an method call matches one of the prototypes, and the resulting state of the monitor, after processing that call, is true, false, or inconclusive, respectively.

Example

Here is an example

PROTOTYPES

void Bank.open(int act);
void Bank.close(int ac);
void Bank.withdraw(int act, int amount);
boolean Bank.isApproved(int act, int amt);

SPEC LTL-FO+
G ([m1 /call/method] (((m1) = ({close})) ->
  ([a1 /call/act/value] (X (G ([a2 /call/act/value]
    (!((a1) = (a2)))))))))

@FALSE {
  System.out.println("The error was successfully caught");
}

© 2010-2011 Jérôme Calvar and Sylvain Hallé. This program comes with ABSOLUTELY NO WARRANTY. This is free software, and you are welcome to redistribute it under certain conditions. See COPYING for details.

Main menu

SourceForge.net Logo