A lightweight approach for the semantic validation of model refinements
Material type:
ArticleSeries: ^p Datos electrónicos (1 archivo : 297 KB)Publication details: ref_localidad@37940 : , 2008Subject(s): Online resources: Summary: Model Driven Engineering proposes the use of models at different levels of abstraction. Step by step validation of model refinements is necessary to guarantee the correctness of the final product with respect to its initial models. But, given that accurate validation activities require the application of formal modeling languages with a complex syntax and semantics and need to use complex formal analysis tools, they are rarely used in practice. In this article we describe a lightweight validation approach that does not require the use of third-party (formal) languages. The approach makes use of the standard OCL as the only visible formalism, so that refinements can be checked by using tools that are fully understood by the MDE community. Additionally, for the efficient evaluation of the refinement conditions a hybrid strategy that combines model checking, testing and theorem proving is implemented. Correctness and complexity of the proposal are empirically validated by means of the development of case studies and a comparison with the Alloy analyzer. -- Keywords: modeling, refinement, model transformation, Object Constraint Language, OCL, MOF, UML, validation, testing, model checking.
| Item type | Current library | Call number | Status | Date due | Barcode |
|---|---|---|---|---|---|
Capítulo de libro
|
Biblioteca Fac.Informática | A0119 (Browse shelf(Opens below)) | Available | DIF-A0119 |
Browsing Biblioteca Fac.Informática shelves Close shelf browser (Hides shelf browser)
Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea (Cons. 09/03/2009)
Model Driven Engineering proposes the use of models at different levels of abstraction. Step by step validation of model refinements is necessary to guarantee the correctness of the final product with respect to its initial models. But, given that accurate validation activities require the application of formal modeling languages with a complex syntax and semantics and need to use complex formal analysis tools, they are rarely used in practice. In this article we describe a lightweight validation approach that does not require the use of third-party (formal) languages. The approach makes use of the standard OCL as the only visible formalism, so that refinements can be checked by using tools that are fully understood by the MDE community. Additionally, for the efficient evaluation of the refinement conditions a hybrid strategy that combines model checking, testing and theorem proving is implemented. Correctness and complexity of the proposal are empirically validated by means of the development of case studies and a comparison with the Alloy analyzer. -- Keywords: modeling, refinement, model transformation, Object Constraint Language, OCL, MOF, UML, validation, testing, model checking.
Electronic Notes in Theoretical Computer Science (ENTCS), 220 (1) : 43--61, 2008.
There are no comments on this title.