Description

The goal of this project is to connect the LTSmin verification toolset to the Java platform. Thus, it should be possible to quickly prototype extensions to LTSmin (which itself was implemented in C/C for legacy reasons). The connection is possible through a conceptually very simple interface which is underlying all LTSmin tools: the PINS dependency matrix.

The LTSmin toolset is a promising verification platform which consolidates several years of research. LTSmin already connects a sizeable number of existing (verification) tools: muCRL, mcrl2, DiVinE, SPIN, NIPS, CADP, GNA. Moreover, it allows to reuse existing tools with new state space generation techniques.

The success story so far is due to a conceptually very clean interface: all LTSmin modules work with a unifying state representation of integer vectors of fixed size, and the PINS dependency matrix which exploits the combinatorial nature of model checking problems. This splits model checking tools into three mostly independent parts: language modules, PINS optimizations, and model checking algorithms.

For example, implementing support for a new language module is in the order of 200-600 lines of C "glue" code, and automatically yields tools for standard reachability checking (e.g., for state space generation and verification of safety properties), reachability with symbolic state storage, fully symbolic (BDD-based) reachability, distributed reachability (MPI-based), and multi-core reachability (in preparation).

On the other hand, the implementation of a verification algorithm based on the PINS matrix automatically has access to muCRL, mcrl2, DVE, PROMELA and ETF language modules.

Finally, all tools benefit from PINS2PINS optimizations, like local transition caching (which speeds up slow state space generators), matrix regrouping (which can drastically reduce run-time and memory consumption of symbolic algorithms).

Problem Statement

The current implementation of LTSmin is for the most part a hairy ball of C code. While the situation is improving steadily, it is still not easy for a newcomer to the project to try out new techniques within the toolset, in particular without prior knowledge of C. With the connection to Java we hope to lower the ramp-up time for newcomers, and also for ourselves.

With Java, we hope to gain access to the plethora of Java libraries and data structures, and quickly prototype high-level implementations of new algorithmic ideas while worrying about performance later.

Note that for the time being, C cannot fully be eliminated from the picture. Some of LTSmin's external dependencies are C-based, and this is unlikely to change. The current LTSmin C implementation basically exposes a sane and unifying, yet still high-performance interface for all PINS language modules.

As final note, we can empirically evaluate the often-made claim that the Java toolchain has caught up with C compilers and provides performance in the same ball park with a much nicer programming experience.

Tasks

This project is (except for the first two steps) modular, i.e., the order choice of steps is not fixed.

• Implement a thin JNI interface to the access integer state vectors provided by the C-based LTSmin. Implement a JNI interface to the PINS matrix. (This gives access to all LTSmin-supported language modules.)
• Design an object-oriented architecture for a Java-based LTSmin toolset, which wraps the above JNI bindings. Finally, utilize the new architecture with simple algorithms (e.g., breadth-first search) written in Java.
• Implement the PINS2PINS local transition caching on the Java side. This reduces the number of costly JNI calls to a minimum. Evaluate the performance.
• Implement (or reuse) symbolic (vector) set data structures of C-LTSmin in Java. Extend this to full symbolic reachability.

References

1. Stefan Blom, Jaco van de Pol and Michael Weber. Bridging the Gap between Enumerative and Symbolic Model Checkers, Technical Report TR-CTIT-09-30, CTIT, University of Twente, Enschede. (2009) (Digital version available here)

Additional Resources

1. The paper