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.
Model Validation through CooML Snapshot Generation / C. Fiorentini, M. Ornaghi (ARBEITSBERICHTE AUS DEM FACHBEREICH INFORMATIK). - In: Tests and Proofs: Papers Presented at the Tests and Proofs: Papers Presented at the Second International Conference / [a cura di] B. Beckert. - [s.l] : Universitaet Koblenz-Landau, 2008. - pp. 17-32 (( Intervento presentato al 2. convegno International Conference on Tests and Proofs tenutosi a Prato nel 2008.
Model Validation through CooML Snapshot Generation
C. FiorentiniPrimo
;M. OrnaghiUltimo
2008
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
2008_tap.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
311.59 kB
Formato
Adobe PDF
|
311.59 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.