Les langages formels de spécification

Les langages formels de spécification

 Les ASTD

La notation ASTD [FGL+08] (Algebraic State Transition Diagram) est une notation graphique formelle combinant le formalisme des diagrammes d’état de Harel et le formalisme de l’algèbre de processus eb3 [FSD03]. Elle est caractérisée par une structure et un état. La structure graphique modélise la sémantique et l’état représente les évolutions de l’astd au cours de son exécution. Des règles de sémantique formelle ont été définies pour les astd. Un astd comporte un état initial, et peut avoir plusieurs états finaux. La structure des astd est décrite inductivement.

Les différents types d’astd sont les suivants : Le type Élémentaire : Le type élémentaire correspond aux places d’un automate. Il ne peut être présent que dans les astd de type automate. Le type Automate : Le type automate reprend le formalisme des diagrammes d’états. Il est constitué d’un ensemble d’états, qui peuvent être des états élémentaires ou un autre astd. Un ensemble de transitions permet de parcourir les états. Les transitions peuvent être gardées. Elles peuvent aussi être franchies depuis ou vers un état d’un automate de niveau immédiatement inférieur à celui de l’astd courant. Enfin il existe des états historiques qui permettent de retrouver le dernier état visité dans un astd. 7 Les langages formels de spécification 

Le type Synchronisation paramétrée 

Ce type d’astd permet de synchroniser deux astd. Il a comme paramètre un ensemble d’événements. Les événements ne faisant pas partie de cet ensemble sont exécutés en entrelacement. Les événements de l’ensemble doivent être exécutés en même temps dans les deux astd. Si l’ensemble de synchronisation est vide, c’est un entrelacement. Le type Synchronisation quantifiée :

La synchronisation quantifiée prend comme paramètre un astd, un ensemble de synchronisation, une variable de quantification et un ensemble de valeurs correspondant aux valeurs possibles pour cette variable. On exécute donc autant d’astd qu’il y a de valeurs dans l’ensemble. Comme pour la synchronisation paramétrée, les événements n’appartenant pas à l’ensemble de synchronisation sont exécutés en entrelacement, les autres sont exécutés en même temps pour l’ensemble des astd. Cette notation peut être étendue : on ajoute comme paramètre un prédicat ; seuls les astd dont les variables de quantification vérifient le prédicat se synchronisent. Le type Séquence : L’opérateur de séquence prend en paramètre deux astd. Le deuxième astd ne peut commencer son exécution que lorsque le premier astd est dans un état final.

Le type Choix

Le type choix prend comme paramètre deux astd et en exécute un au choix de l’utilisateur. Le type Choix quantifié : Le choix quantifié prend comme paramètre un astd, une variable de quantification et un ensemble de valeurs possibles pour la variable de quantification. Il permet d’exécuter l’astd en paramètre pour une des instanciations de la variable de quantification. Le type Garde : Un astd de type garde ne peut être exécuté qui si sa garde est vérifiée. Le type Appel d’ASTD : Le type appel exécute l’astd appelé, auquel on peut passer des paramètres. Le type Fermeture de Kleene : Un astd de type fermeture de Kleene spécifie le fait qu’on puisse exécuter plusieurs fois un astd, y compris zéro fois. 

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 substitution “affectation” qui affecte une valeur à une variable ; — La substitution “devient tel que”, une substitution non déterministe qui spécifie la modification d’une variable de telle manière qu’elle vérifie une propriété écrite sous la forme d’un prédicat B ;