Introduction

Model checking has been successful at verifying safety and liveness properties of systems with very large state spaces. However, model checking requires the programmer to write and maintain a model of the system, separate from the actual implementation. If the model does not match the system, the model checker could give false alarms, or worse, it could fail to detect actual bugs in the system.

One way to ease the task of writing the model is to make sure the specification language is expressive enough to concisely model the structures and operations in the system. Most of the existing tools have poor or no support for models containing relations and expressive relational operators. Previous work on Alloy has shown that relational operators can often be used to succinctly describe behaviors and operations on structural objects. Without expressive relational operators, programmers are required write verbose specifications that are more likely to contain errors.

Furthermore, traditional model checking tools requires all state transitions to be described explicitly. It is not enough to only describe the desired effect of a state transition: an implementation describing how the state changes has to be provided. As a result, the model specification is often verbose, and this increases the likelihood that there is a bug in the specification, or that the specification and the actual system do not match.

Approach

This research aims to blend the strength of traditional model checkers with the expressiveness of a declarative, relational language. The goal is to enable programmers to write very intuitive and compact specifications, in order to allow the automatic verification of more complicated software systems. The key idea is that many structural operations (common in object-oriented programs) can be easily described using relations and relational operators, while other operations are best described using the primitive data types and their operations (such as simple arithmetic operations on numbers). By allowing a mixture of both, and by allowing parts of the model to be described declaratively rather than imperatively, the programmer has the freedom to model each part of the system differently, using the most intuitive and simple constructs.

Progress

We have designed a prototype for a specification language that combines the strength of traditional model checkers with the expressiveness of a declarative relational language. And we have built a proof-of-concept BDD-based model checker for the language, and successfully verified several algorithms, including the core dependency algorithm in Apache Ant for up to 5 nodes.

Future Work

We hope to apply our techniques to embed relational data types into state-of-the-art model checkers and augment them with expressive relational operators.

Research Support

This work is supported in part by grant 0086154 (Design Conformant Software) from the ITR program of the National Science Foundation.

References

[1] Felix Sheng-Ho Chang and Daniel Jackson. Symbolic Model Checking of Declarative Relational Models. Submitted to Foundations of Software Engineering (FSE), Lisbon, Portugal, September 2005.