A Multi-formalism Approach for the Validation of UML Models |
| |
| Authors: | Sophie Dupuy Lydie du Bousquet |
| |
| Affiliation: | (1) Laboratoire LSR-IMAG, Saint Martin d'Hères, France, FR |
| |
| 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. Received February 2000 / Accepted in revised form December 2000 |
| |
| Keywords: | : Lustre Multi-formalism Rational Rose™ RoZ UML Z-EVES Z |
| 本文献已被 SpringerLink 等数据库收录！ |
