Règles de simplification des astd

Règles de simplification des astd

Lors de la modélisation d’un système en utilisant la méthode présentée dans le chapitre 2, il est nécessaire de prouver la cohérence de la modélisation. Pour rappel, le système est spécifié en deux parties. D’une part, une spécification astd modélise l’agencement des actions et d’autre part, une spécification Event-B spécifie les modi f ication qu’apportent ces actions au modèle de données. Les événements du modèle de données peuvent être gardés.

Prouver la cohérence de la spécification consiste à montrer que lorsqu’une transition doit être exécutée (selon la spécification astd), les variables d’état caractérisant les données du système sont dans un état permettant l’exécution de l’événement Event-B correspondant (les variables d’état satisfont la garde). Pour cela, les astd sont traduits en langage B et l’événement modélisant les modifications apportées au modèle de données est appelé dans l’opération qui est la traduction de chaque étiquette de transition.

Dans la traduction des astd en langage B, l’état des astd est codé par un ensemble de variables d’état et le nombre de va riables d’état nécessaires croît en même temps que le nombre de niveaux hiérarchiques de l’astd. Plus l’astd aura de niveaux hiérarchiques et plus la relation entre les va riables d’état associées à l’astd et les variables d’état associées à la modélisation de données sera complexe.

L’objectif de ce chapitre est de présenter quelques règles de simplification des astd pour simplifier les preuves en B associées à la modélisation.  L’objectif de ce chapitre n’est cependant pas de proposer des règles systématiques permettant de réduire le nombre de niveaux hiérarchiques de tous les astd, notam ment pour les deux raisons suivantes :

— Tousles types d’astd ne sont pas simplifiables. Il est très compliqué de traduire une synchronisation quantifiée en automate par exemple : l’automate contien drait toute les combinaisons d’entrelacement possible pour toute les variables de l’ensemble de quantification. — Certaines “simplifications” diminuant le nombre de niveaux hiérarchiques aug mentent en pratique la complexité de la modélisation.

Dans le cas de la mo délisation présentée à la figure 4.1 par exemple, le seul moyen de diminuer le nombre de niveaux hiérarchiques est de faire partir la transition t2 de tous les sous états de S1. Dans la spécification de départ, il faut vérifier que l’état de l’astd est S1. Dans la spécification d’arrivée, la condition pour exécuter t2 est une disjonction de quatre conditions. Dans ce chapitre nous proposons donc un catalogue non exhaustif de règles que nous avons jugées utile d’appliquer dans nos cas de modélisation.

Ces règles sont au nombre de trois. La première concerne les fermetures de Kleene (section 4.3), la deuxième l’opérateur de choix (section 4.4) et la troisième la simplification des automates (section 4.5). Les règles permettant de réécrire l’opérateur de choix et la fermeture de Kleene s’appliquent à des automates dont aucune transition n’arrive à l’état initial.

Nous définissons donc également une règle qui permet de transformer un astd ayant une transition arrivant à l’état initial en un astd sans transition arrivant à l’état initial (section 4.2). Ce catalogue pourrait évidemment être complété suivant 104 4.1. Introduction les besoins de futurs cas. Ces règles de réécriture ont été écrites avec Étienne Corbillé, dans le cadre d’un stage de fin d’étude au sein de l’entreprise Ikos Consulting.

Enfin, nous rappelons que l’objectif de ces règles est de réécrire les spécifications astd afin de faciliter les preuves après la traduction en langage B. Les spécifications obtenues après réécriture ne sont donc généralement pas plus lisibles. Cependant, ces règles ont été traduites en OCamL et ont été intégrées à l’outil de traduction des astd vers le langage B. Les réécritures sont donc transparentes pour la personne qui modélise le système.