Modal Object Diagrams

TL;DR

This paper introduces modal object diagrams (MODs), an extension of object diagrams with modalities to specify positive/negative examples and invariants, and provides a formal verification method using Alloy.

Contribution

The paper presents MODs, an expressive extension of object diagrams with modalities, and a verification technique for class diagram conformance, implemented as an Eclipse plugin.

Findings

MODs allow specifying positive and negative examples and invariants.

The verification technique reduces to Alloy for decision procedures.

Prototype implementation demonstrates practical usefulness.

Abstract

While object diagrams (ODs) are widely used as a means to document object-oriented systems, they are expressively weak, as they are limited to describe specific possible snapshots of the system at hand. In this paper we introduce modal object diagrams (MODs), which extend the classical OD language with positive/negative and example/invariant modalities. The extended language allows the designer to specify not only positive example models but also negative examples, ones that the system should not allow, positive invariants, ones that all system's snapshots should include, and negative invariants, ones that no system snapshot is allowed to include. Moreover, as a primary application of the extended language we provide a formal verification technique that decides whether a given class diagram satisfies (i.e., models) a multi-modal object diagrams specification. In case of a negative answer, the technique outputs relevant counterexample object models, as applicable. The verification is based on a reduction to Alloy. The ideas are implemented in a prototype Eclipse plug-in. Examples show the usefulness of the extended language in specifying structural requirements of object-oriented systems in an intuitive yet expressive way.