A small demo: monitoring Java programs with BeepBeep

Overview

Using BeepBeep, you can monitor properties on sequences of method calls inside a Java program.

An example

Consider the following method declarations for a simple Java class called Bank:

class Bank
{
  public void open(int accountNo) {...}
  public void close(int accountNo) {...}
  public void withdraw(int accountNo, int amount) {...}
  public boolean isApproved(int accountNo, int amount) {...}
}

Suppose that the use of these methods is subject to the following constraints:

  1. An account cannot be closed until it is opened
  2. No operation on an account can be made after close
  3. Any withdrawal over $1,000 requires an approval first
  4. The amount cannot change between an approval request and the following withdraw

Hence the following sequences of operations are forbidden:

All these scenarios should provoke an error related to either of the three constraints mentioned above.

Using BeepBeep

Using BeepBeep, one can define a property and have it automatically monitored in parallel with the execution of the actual program. This is done by writing a specification, which is translated into an AspectJ class called the EventFormatter by an online script.

You start by telling the monitor which method calls to trap by providing their prototypes:

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);

Remark that you must give the method's complete signature, including the class it belongs to. The prototypes allow you to name method arguments --note that the parameters don't need to have the same name as their declaration in the original source code (see how account in the Bank's source becomes act in the first prototype and ac in the second). You give them the names you want.

Every time one of these methods is called, the EventFormatter creates an event, which is a simple XML structure providing information about that particular method call. For example, here is the XML document produced for the call b.withdraw(123, 2000):

<call>
  <method>withdraw</method>
  <act>
    <type>int</type>
    <value>123</value>
  </act>
  <amount>
    <type>int</type>
    <value>2000</value>
  </amount>
</call>

Each call contains a method tag giving the method's name, and a sequence of arguments elements providing information about the call's arguments. In this case, the first element tells us that argument act, of type int, has a value of 123. Similarly, the second element tells us that argument amt is the int 2000. The names of each argument are those you provided in the prototype declaration for this particular signature.

Writing constraints in LTL-FO+

LTL-FO+ is an extension of Linear Temporal Logic (LTL) and includes the same temporal operators and Boolean connectives.

As an example, Constraint 2 becomes in LTL-FO+:

Gm1 /call/method : (m1 = close → ∀ a1 /call/act/value : X Ga2 /call/act/value : a1a2)

Read the documentation for LTL-FO+ to learn how to express constraints.

The next step is to provide these constraints to the EventFormatter. Currently you can give only one LTL-FO+ formula for the sentinel to watch. This is done by adding a second section to the specification file as follows:

SPEC LTL-FO+

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

Here we chose to put formula 2. The formula is identical, except that a universal quantifier ∀ x /p/p/p is written as [x /p/p/p], and that any subexpression must be strictly enclosed by parentheses, down to single variables. In addition, constants must be enclosed by braces (see close above) to be recognized as such. (The underlying monitor used by the sentinel is picky about the textual syntax and will stop working at the slightest divergence.)

Recovery code

The last part of the specification provides code that is to be executed whenever the monitor discovers a violation. This is done by writing @FALSE, followed by any number of lines of Java code:

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

A formula can also specify an undesirable property; in such a case, one can enter code when the property is satisfied using the equivalent @TRUE construct.

Putting it all together

Here is the complete EventFormatter specification for property 2:

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");
}

Input this whole text into the online form and click on Submit. The plugin generates an AspectJ file that is ready to be inserted into your original project.

To summarize: the monitoring process

  1. A user writes an input specification describing the method calls to intercept and the property to monitor on the sequence of calls.
  2. A PHP script transforms the input specification into an executable AspectJ file called the EventFormatter.
  3. The EventFormatter creates an instance of a runtime monitor called BeepBeepMonitor. Upon each event caught, it generates an XML document from the call's parameters and passes it to the monitor for verification.
  4. According to the monitor's outcome for an event, the EventFormatter can execute some recovery code given in the input specification.

A separate .jar file, beepbeep.jar, contains the code for the BeepBeepMonitor and must be linked to the original project, along with the generated AspectJ file.

Specifics

For more information

Main menu

SourceForge.net Logo