Activity: Integration of UML and formal notations

Location: London (England)

Date: May 17th- August 20th

Proposer: Sophie Dupuy

Member: LSR-IMAG

I visited Anthony Finkelstein's group at UCL. The purpose of the visit was to study the integration of the Z formal notation and UML notations by defining consistency rules between UML and Z.

This work presents a different approach than the one (translation process) I used in previous work and allows to compare the two approaches to integrate formal and semi-formal notations. The two sets of rules to integrate the UML and the Z formalisms have been compared.

Moreover the consistency rules between UML and Z are used to identify some types of rules that are not supported by the consistency checker proposed by Anthony Finkelstein's group and to propose some extensions for the tool. One of the them (disjunctions between conditions of consistency rules) has been implemented.