Les étapes pour la traduction automatique de la spécification Z et réseau de Petri en Aspects.

1- Ouvrir le fichier XML généré à partir d’une modélisation du réseau de Petri. (File -> Load Xml)

Cette étape n'est pas nécessaire si nous n’avons pas modélisé le protocole de coordination par un réseau de Petri.

Exp: Vous trouver le fichier "CAS Petri net.xml" dans le répertoire "Petri Net".

2- Ouvrir le fichier Latex (Z) généré à partir d'une spécification formelle Z. (File -> Load Z)

A cette étape, un fichier XML sera généré automatiquement pour vérifier la structure de la spécification selon le méta model.

Le fichier XML est généré dans le répertoire courant sous le non "Zspecification.xml". Le méta model (XML schema) est aussi généré dans le même répertoire courant sous le nom "MetaModel.xsd".

Exp : vous trouver les spécifications dans le répertoire "Z Specification".

3- Valider la structure de la spécification selon le MetaModel (Meta-Model -> Check)

4- Visualiser le fichier XML généré ainsi que le MetaModel (Meta-Model -> View -> Z2XML file ou XSD file).

5- Créer un squelette du fichier XML permettant de faire le Mapping de la specification avec le code (AOP -> PointCut -> Map PointCut).

Ce squelette sera généré sous le nom "Mapping" sans le répertoire "Mapping".

Exp: Les autres exemples sont déjà crée dans le répertoire "Mapping/Mapping pour TestCAS".

6- Visualiser le fichier Mapping (AOP -> PointCut -> Map PointCut).

7- Générer les aspects, il faut choisir l'emplacement des aspects (AOP -> Generate Aspects).