A Multi-formalism Approach for the Validation of UML Models

Abstract
: Our approach is based on UML models. They are edited with the rational Rose tool [Rat96] and complemented with annotations that state several constraints. The class diagram is the starting point of a translation process that produces formal specifications in Z [Spi92] and Lustre [CHP87]. The RoZ tool is used to translate the class diagram into Z automatically. The Z and Lustre specifications are used to validate the UML models by means of a prover and a testing environment.

This publication has 0 references indexed in Scilit: