Checking the consistency of models is vitally important for the success of model-driven development. For the correct operation of tools, it is essential to be able to check that a given model conforms to the rules imposed by its metamodel. Checking for consistency among different views of a model may avoid some costs of fixing a problem too late.

This paper explores several approaches to checking model-to-metamodel consistency and multiview consistency. The exploration is centered on choosing the right notation and formalism to define the metamodel, and to express the model and its views in the metamodel. The exploration is illustrated with the business object notation (BON) modeling language, which is similar to unified modeling language (UML) 2.0, and each modeling step is related to its respective counterpart in UML 2.0.

The authors consider three different notations: BON (as an informal diagrammatic notation), prototype verification system (PVS) (as a very formal notation), and Eiffel (as a programming language also suitable for formal specifications), with the latter two explored in detail. The paper elaborates on the pros and cons of each of the approaches. Both PVS and Eiffel win on tool support; PVS loses on understandability and automation (even though it wins on expressiveness), while Eiffel wins on understandability, maintainability, and automation, at the expense of expressiveness.

The paper would be particularly suitable for designers of modeling languages (including domain-specific languages) who would like to create a formally based metamodel for their modeling language. The target audience, however, also includes tool developers considering the development of a formally based metamodel for an existing language, to add support for checking metamodel-to-model and multiview consistency. For the general audience, the paper provides an overview of the metamodeling field, and demonstrates how PVS and Eiffel can be used for consistency checking.