MV : A Tool for Reliable Monitor Development

We present a tool for reliable monitor development. Our tool has a modular approach to specification and verification of monitors by decoupling the behavior and the interface specifications. For the behavior verification we use infinite state verification techniques which enables us to verify a monitor with parameterized constants and arbitrary number of user threads. We automatically generate Java monitors from the input specifications which preserve the verified properties. For the thread verification we use finite state program verification tools which enables us to verify Java threads without any restrictions. The correctness of the user threads is verified using stubs generated from the monitor interfaces instead of the monitors themselves which improves the efficiency of the thread verification significantly. Our tool implements refinement checks which enables the users to design complex monitors by composing interfaces of different monitors.

There are two main approaches to model checking concurrent systems:

Specification Checkers
Specification checker tools use symbolic representations to represent transition relation and sets of states of a system instead of enumerating them. Using such symbolic representations they are capable of verifying very large (and even infinite) state spaces. However, they are not capable of handling all features of a high-level programming language. They can only verify constructs that can be represented by the symbolic representations they use.
Program Checkers
Program checkers are explicit state model checkers and verify concurrent programs written in programming languages such as C or Java. Program checkers with explicit state representations are capable of checking arbitrary programs without any restrictions. However, explicit state model checkers are not able to handle infinite state spaces and are mostly used to perform a partial state space search.

We use both symbolic and explicit state automated verification techniques by exploiting the separation between the behavior and the interface of a monitor. We use an infinite-state specification checker (Action Language Verifier ) for the verification of component behaviors. We use a program checker (JPF ) for the verification of the thread behavior.

Usage

To create an Action Languge specification with N threads
```
 MV -a N infile 
```
To create an Action Languge specification using counting abstraction
```
 MV -a 1 -A infile 
```
To create an Java monitors and stubs
```
 MV -G infile 
```
To do invariant preserving refinement check
```
 MV -i infile 
```
To do ACTL preserving refinement check
```
 MV -c infile 
```

MV accepts any combination of these flags.

Here are some examples:

System requirements:

Sun Sparc machines
Action Language Verifier
Java Path Finder

Download executable here