Model Validation through CooML Snapshot Generation

The object of this paper is model validation, namely the study of the “correctness” of formal specifications (or models) with respect to their requirements. Since requirements are informal, validation can be only experimental. In the UML, snapshot generation has been proposed as a tool for validating class diagrams and contracts. Snapshots are object diagrams representing the possible system states, where one compares the snapshots generated from the UML model with the expected ones. In this paper we present a DLV implementation of snapshot generation for CooML (Constructive Object Oriented Modeling Language), a modeling language based on a constructive semantics we are developing.We firstly explain CooML snapshot semantics and we show by an example how UML class diagrams with OCL constraints can be represented in CooML. Then we explain our implementation of CooML snapshot generation in DLV and discuss its potential application for model validation.