Définition formelle d’une méthode de spécification couplant astd et B

Définition formelle d’une méthode de spécification couplant astd et B

La méthode de spécification combine les langages B et Event-B et la notation graphique astd. La méthode est résumée à la figure 2.1. Les astd permettent de modéliser l’ordonnancement des actions grâce à une notation graphique et aux opé- rateurs des algèbres de processus (rectangles de gauche sur la figure 2.1). Cependant, cette modélisation ne permet pas de spécifier les modifications apportées par chaque transition au modèle de données. Ces modifications sont spécifiées en utilisant le lan- gage Event-B (rectangles de droite sur la figure 2.1). Enfin, pour vérifier la cohérence de la spécification, les deux spécifications sont traduites en langage B (rectangles cen- traux sur la figure 2.1). Le choix des différents langages sera discuté dans la section 2.2. Le raffinement combiné des deux méthodes est décrit dans la section 2.3.La spécification astd permet de modéliser l’agencement des actions. Puisque les astd sont basés sur les diagrammes de transition d’états, ils permettent d’écrire une spécification graphique qui peut être relue, comprise et validée facilement. De plus, les opérateurs des algèbres de processus permettent non seulement d’ajouter de la lisibilité en factorisant certaines spécifications (fermeture de Kleene, opérateur de séquence), mais également d’ajouter de la puissance d’expression en étendant un comportement à un ensemble de processus (synchronisation et choix quantifiés). Enfin, les astd sont définis grâce à une sémantique formelle (définie dans [FGLF08]), qui permet d’éviter les ambiguïtés.

La spécification astd ne permet de spécifier qu’un agencement d’actions. Pour que la méthode puisse décrire le fonctionnement d’un système, il est nécessaire de pouvoir décrire l’effet de ces actions sur les données du système. Cet effet est décrit par le langage Event-B, qui est un langage de spécification basé sur les états. La principale raison du choix d’Event-B, par rapport au langage B classique, est de faciliter le raffinement des spécifications. En effet, le raffinement Event-B permet l’ajout d’événements, comme le raffinement astd permet l’ajout de transition.La machine Event-B associée à un astd contient un ensemble de variables d’état et contient un événement pour chaque étiquette de transition de la spécification astd. L’événement associé à une étiquette de transition permet de décrire l’effet de cette transition sur les variables d’état du système. C’est généralement dans cette partie de la spécification que seront traduites les propriétés que doit vérifier le système, généralement au moyen d’invariants. Ces invariants ne permettent pas d’écrire tous les types de propriétés, même si certaines (comme certaines propriétés utilisant des opérateurs de la logique temporelle) peuvent être encodées au moyen de théorèmes du langage Event-B.La spécification astd spécifie l’agencement des actions, c’est-à-dire qu’elle spécifie le moment où doivent être exécutées les transitions.

La spécification Event-B spécifie les changements apportés aux données du système lors de chaque transition. Cepen- dant, pour permettre la préservation des propriétés de sûreté écrites sous la forme d’invariants, les événements Event-B ont une garde qui doit être vraie au moment d’exécuter l’événement. La spécification en B classique permet de vérifier que lors- qu’une action peut être exécutée selon la spécification astd, la garde correspondante en Event-B est vraie.Pour vérifier cela, les deux spécifications sont traduites en B classique. L’idée de la traduction des astd est la suivante : les états des astd sont codés par des variables d’état en B. Une opération B est créée pour chaque étiquette de la spécification astd. La précondition de l’opération vérifie que les variables d’état correspondent à l’état précédant la transition. La postcondition met à jour les variables pour qu’elles correspondent à l’état qui suit la transition.De même, la spécification Event-B est traduite en B classique. Les variables et in- variants de typage sont conservés. Les gardes de chaque événement sont transformées en précondition et les postconditions restent inchangées. Chaque opération résultant de la traduction de la machine Event-B est appelée dans l’opération qui résulte de la traduction en B de l’étiquette de transition correspondante. Les obligations preuvesDans cet exemple, nous souhaitons modéliser le contrôle de la température d’une voiture par un système de climatisation.

L’utilisateur peut entrer une température souhaitée, dont le système doit se rapprocher, mais pour éviter que la différence de température avec l’extérieur soit trop importante, il peut décider de définir un écart maximal avec la température extérieure. Avant de décider s’il doit mettre en route ou non la climatisation, le système doit donc connaitre les deux températures. Pour cela, il dispose de deux mesures de température : la première est une mesure de la température à l’intérieur et la seconde une mesure de la température à l’extérieur. Le système relève d’abord la température de l’intérieur de l’habitacle, puis la température de l’extérieur. Il décide ensuite s’il doit déclancher la ventilation chaude ou froide ou s’il ne doit rien faire.