Les langages formels de spécification

La méthode B

La méthode B [Abr96] est une méthode de spécification formelle du logiciel. Elle permet de décrire formellement un système de sa spécification abstraite jusqu’à son implémentation. Son formalisme repose sur des notions mathématiques de la théorie des ensembles et de la logique du premier ordre. Elle se base également sur une relation qui permet de relier une machine abstraite à une machine concrète qui détaille la spécification de la machine abstraite. Cette relation, appelée raffinement, doit être prouvée par des obligations de preuves, afin que les propriétés des machines soient conservées. La méthode est outillée notamment grâce à l’atelier B 1 qui permet d’éditer la spécification, qui génère les obligations de preuves et qui permet de prouver ces obligations à l’aide de différents prouveurs.
Une spécification B contient plusieurs MACHINES. Une machine spécifie des opérations qui modifient les données. Elle contient également une partie statique qui contient les propriétés du système. Les propriétés sont écrites sous la forme d’invariant ou d’assertion. Les invariants sont des propriétés sur les variables (incluant leur typage). La méthode requiert de prouver que les invariants ne sont pas violés par l’exécution de chaque opération. Les assertions sont des lemmes facilitant la preuve de invariants et qui doivent être prouvées en utilisant les invariants.
Les opérations sont spécifiées par des substitutions sur les variables. Il existe une substitution particulière, la substitution “précondition”. Cette substitution ne peut être utilisée qu’au niveau supérieur d’une opération. Elle est constituée d’un prédicat et d’une substitution. Le prédicat est appelé précondition, la substitution postcondition. Elle signifie que le comportement de la machine n’est connu que si la précondition est vraie. L’ensemble des substitutions utilisables dans la postcondition est défini dans [Abr96]. Nous ne détaillerons ici que les substitutions utilisées le plus fréquemment dans nos travaux.

La méthode Event-B

La méthode Event-B est une méthode dérivée de la méthode B, mais utilisée pour une spécification événementielle. Elle permet de spécifier un système d’événements.
Une partie statique, appelée contexte, définit les constantes et des propriétés sur ces constantes. Une partie dynamique, appelée machine, définit les variables, les invariants et variantssur ces variables, et les événements qui peuvent les modifier. Elle utilise un langage et des clauses très proches de la méthode B. La différence réside essentiellement dans la méthode de spécification.
Comme une machine B, une machine Event-B peut être raffinée. La méthode du raffinement en Event-B suit le “paradigme du parachute”. Selon ce paradigme, le système est spécifié comme si une personne le décrivait pendant une descente en parachute. Le niveau abstrait du système décrit un système très simple et les détailssont ajoutés au fur et à mesure des raffinements.
La machine Event-B contient des événements, dont un événement d’initialisation, qui remplacent les opérations de la machine B. Les valeurs d’initialisation doivent établir les invariants. Un événement peut être paramétré, à l’aide d’une clause ANY.
Une clause WHEN permet d’associer une garde à l’événement. Un événement ne peut être déclenché que si toutes ses gardes sont vraies. Les actions sont décrites dans une clause THEN. Contrairement au B classique, on ne peut écrire pas écrire de substitutions imbriquées, telles que les SELECT. On ne peut écrire que des affectations et des substitutions “Devient tel que”.
Le calcul des obligations de preuve n’utilise pas la théorie des substitutions généralisées. Les clauses de la machine (invariants, gardes, substitutions, etc…) sont exprimées par des prédicats liant les différents éléments de la machine (variables, constantes, paramètres, etc…). Les obligations de preuves demandent de déduire certains de ces  prédicats à partir d’autres, suivant les règles définies dans [Abr07]. La preuve des obligations de preuves permet de garantir, comme pour le B classique, la préservation des invariants et les raffinements. Les obligations de preuve de l’Event-B demandent à prouver en plus la faisabilité de la substitution. Pour une substitution de type “Devient tel que”, cette obligation consiste à montrer que pour chaque variable modifiée, il existe une valeur qui satisfait le prédicat.

Le raffinement

Les systèmes ferroviaires sont des systèmes complexes. Pour faciliter la spécification, nous souhaitons pouvoir modéliser les systèmes en plusieurs étapes. Les premières spécifications sont dites abstraites et ne modélisent pas tous les détails dufonctionnement du système. Ces détails de fonctionnement sont spécifiés dans desmodélisations ultérieures. Une relation de raffinement permet de garantir la cohérence entre deux niveaux de modélisation. Cette relation est définie par unensemble de propriétés qui doivent être prouvées pour prouver le raffinement d’une spécification par une autre.

Les spécifications basées sur les événements

Dans les algèbres de processus, comme CSP [Hoa78], les observations sur le système sont faites à l’aide de séquences d’événements admises ou non par la spécification. On observe plusieurs ensembles de séquences d’événements, telles que les traces, les séquences menant à un deadlock, les séquences divergentes, etc… Dans ce type de spécification, un raffinement est définipar des relations d’inclusion ou d’égalité entre ces ensembles. On parle de sémantique dénotationnelle [RHB97]
Ces ensembles définis ci-dessus correspondent à une modélisation des comportements admissibles du système. L’idée général du raffinement de système décrit par un paradigme basé sur les événements est la suivante. Il ne faut pas qu’une machine concrète C qui raffine une machine abstraite A admette des comportements que n’admet pas A. Il faut donc que les ensembles décrivant le comportement de la machine
C soient au moins admis par la machine A. On peut par exemple comme le font Schneider et al. [STW14] définir le raffinement en CSP de la manière suivante.

Les spécifications basées sur les états

Les méthodes de spécification basées sur la représentation des états des variables définissent des types de donnée abstraits (Abstract Data Types – ADT). Un ADT [DB01] est défini par une initialisation et un ensemble d’opérations. L’initialisation permet de définir l’état initial des variables et les opérations peuvent être vues comme des relations entredes états des variables. Dans ce système de représentation, les raffinements sont exprimées àl’aide d’une relation de simulation. La relation de simulation lie les états de la machine concrète à ceux de la machine abstraite. Si on effectue une même opération dans des états liés par la relation de simulation, les nouveaux états obtenus doivent être liés par la relation de simulation. C’est le cas pour la définition du raffinement en B et Event-B : le raffinement n’est pas défini par une relation sur les comportements globaux du système, mais par une relation liant la transformationabstraite des états à la transformation concrète.

Le Raffinement de la méthode B

Nous l’avons vu dans la section 1.1.2, dans une machine B sont définies des variables. Des opérations permettent de modifier l’état de ces variables tout en ne violant pas les invariants. Soit une machine abstraite A comprenant des variablesva1, va2, …, van, un invariant Ia(va1, va2, …, van) (on considère un invariant global quiest la conjonction de tous lesinvariants), et des opérations op1, op2, …, opk. Soit unemachine concrète C raffinant la machine A.
Le raffinement défini par la méthode B ne permet pas de modifier le nombre d’opérations. Lamachine C contient donc les même opérations op1, op2, …, opk dont on peutmodifier la substitution. La machine C définit de nouvelles variables vc1 , vc2, …, vcm et un invariant Ic(va1 , va2, …, van , vc1 , vc2 , …, vcm) qui lie les variables concrètes aux variables abstraites. Les invariants qui permettent de lier l’état d’une variable concrète à l’état d’une variable abstraite sont appelés invariants de collage. Ce sont ces invariantsqui définissent la relation de simulation.
Une machine B raffine une autre machine B si chaque opération concrète raffine l’opération abstraite correspondante. Informellement, une opération concrète opic raffine une opération abstraite opia si on peut remplacer l’opération opia par l’opération opic sans qu’un observateur ne s’en rende compte. Supposons que les deux opérations sont des substitutions “précondition” de la forme PRE P ra THEN Sua END pour opia et PRE P rc THEN Suc END pour opic (on peut toujours se ramener à une substitution précondition en prenant P r = TRUE). Pour que l’opération opic raffine l’opération opia il faut que la précondition P rc soit moins restrictive que la précondition P ra (i.e. P ra ⇒ P rc) et que la substitution concrète ne contredise pas la substitution abstraite. Si on prend un prédicat R, cela signifie, dans le calcul des plus faibles préconditions que la plus faible précondition qui permet de satisfaire le prédicat R après l’application de la substitution abstraite Sua implique la plus faible précondition qui permet de satisfaire R après l’application de la précondition concrète Suc (i.e. [Sua]R ⇒ [Suc]R). Dans la pratique, cela signifie qu’on réduit le non déterminisme de l’opération, c’est-à-dire que les comportements prévus par la machine concrète sont des comportements prévus par la machine abstraite.

Discussion et positionnement

Pour exprimer la relation de raffinement dans le cadre d’une spécification basée sur les événements, les observations sont faites sur des comportements globaux du système(ensemble de séquences d’événements acceptables, etc…). La définition du raffinement impose donc la vérification de propriétés sur ces comportements globaux du système.
Lorsque les spécifications sont basées sur les états, les observations sont faites sur des opérations modifiant les états du système. Le raffinement impose de vérifier que les modifications qu’effectue une opération concrète sur l’état des variables n’introduit pas d’incohérence avec les modifications qu’effectue l’opération abstraite.Mais la sémantique utilisée pour décrire le comportement ne change pas le sensdonné au raffinement. Schneider et al. [STW14] ont montré par exemple qu’il est possible d’exprimer le raffinement Event-B en matière de traces, divergences et traces infinies. Le choix d’une méthode de spécification et de raffinement par rapport à une autre se fait surtout en fonction du type de comportement que nous souhaitonsreprésenter.
Certaines différences techniques cependant permettent de faire des choix. Le raffinement des astd permet l’ajout d’opérations pendant le raffinement (et l’oblige même d’après [FGLM14]). Nous souhaitons combiner cette méthode à une méthode permettant une expression de la modification des états des variables du système. La méthode B classique ne permettant pas l’ajout d’opération pendant le raffinement, nous privilégierons la méthode Event-B.
Enfin, les astd sont un langage de spécification basé sur les états. Les obligations de preuve du raffinement sont exprimées en utilisant la sémantique dénotationnelle, c’est-à-dire à l’aide de propriétés sur les observations. Pour garantir la sécurité des systèmes ferroviaires, le comportement des entités du système est souvent contraint par un contrôleur. La spécification d’un système ferroviaire pour le cas d’étude [Fay14] a montré que la définition du raffinement donnée dans [FGLM14] est trop restrictive pour permettre de contraindre le fonctionnement d’un système par l’ajout d’un contrôleur.

Les combinaisons de méthodes formelles

iUML-B

La version actuellement développée utilise la méthode Event-B.

Description de la méthode

iUML-B est la combinaison de la notation UML et de la méthode Event-B. Il est intégrée à Rodin, l’outil de spécification en Event-B. Lors de la spécification d’unemachine ou d’un contexte Event-B, il est possible d’ajouter une ou plusieurs machines à états ainsi qu’un ou plusieurs diagrammes de classes. Ces spécifications en UML sont ensuite traduites en Event-B et permettent de contraindre l’exécution de la machine.
La partie de la spécification Event-B résultant directement de la traduction ne peutêtre modifiée, mais d’autres spécifications peuvent être ajoutées.
Les diagrammes de classes permettent de spécifier les structures de données de lamême manière que dans la programmation orientée objet. Il est possible de définir des classes et de leur associer des attributs, des méthodes et des contraintes. On peut également hiérarchiser les types et définir des associations entre des classes. Dans la traduction en Event-B, ces associations sont modélisées par des relations sur les ensembles et les méthodes de chaque classe sont des événements qui permettent de modifier ces ensembles.
Les machines à états s’inspirent des diagrammes d’états de Harel [Har87]. Ils permettent de définir un ensemble d’états et de les relier par des transitions. Dans la traduction en Event-B, les transitions sont traduites par des événements. Les états peuvent être codés de deux manières différentes. Dans la première, ils sont définis comme des constantes, et une variable d’état prend la valeur de l’état courant. Dans ce cas, la garde de la transition vérifie que le système est dans l’état précédant la transition et la postcondition met à jour l’état. Dans la seconde, les états sont définis comme des variables booléennes, qui prennent la valeur vraie s’ils sont l’état courant de l’automate. Les machines à états peuvent être hiérarchiques, c’est-à-dire que l’état de chaque machine à états peut à son tour être une machine à états. Ces machines à états peuvent également avoir plusieurs instances, ce qui permet de spécifier un entrelacement quantifié, mais uniquement au plus haut niveau.
Il n’existe pas de documentation sur les règles de traduction implémentées dans l’outil UML-B. Il est donc difficile de connaître avec précision la sémantique formelle formelle d’une spécification UML. Il faut utiliser l’outil pour voir le code Event-B généré.

Positionnement

La méthode iUML-B est une méthode de spécification très proche des astd. Elle a l’avantage d’être bien outillée et intégrée à Rodin. Cependant, le manque de documentation sur la sémantique formelle ne permet pas de commenter avec précision lesdifférences exactes avec les astd. Certains opérateurs des astd ne sont néanmoins pas inclus dans le langage iUMLB. Il est ainsi impossible de spécifier une synchronisation quantifiée, et l’entrelacement quantifié n’est utilisable qu’au plus haut niveau de spécification.