KORRIGAN : Spécification formelle et structurée de systèmes mixtes

Abstraction

              L’abstraction est une propriété importante puisque des formalismes présentant un plus grand degré d’abstraction conduiront à des spécifications plus concises et plus aisées à valider. Un faible niveau d’abstraction peut ainsi conduire par exemple à une explosion du nombre d’états d’une spécification à base de système états/transitions et rendre impossible sa validation. Nous reviendrons sur ce point (différents types d’explosion d’états) lors de la présentation de notre modèle. L’abstraction aide le spécifieur à ne s’attacher qu’aux points importants par rapport à un problème ou à une propriété donnée. Cependant, l’implémentation (par exemple pour faire un prototype) d’une spécification écrite à l’aide d’un formalisme très abstrait peut présenter beaucoup plus de difficulté. Dans un cadre dynamique, la sémantique d’un formalisme est dite pleinement abstraite quand elle ne contient pas de détails (d’implémentation) non nécessaires. Les composants pleinement abstraits sont décrits en termes de comportements externes (leur interface). La notion de pleine abstraction nécessite la définition de relations d’équivalence ou de congruence spécifiques (par exemple l’équivalence observationnelle [205] pour les processus). La compatibilité de composants et une forme de sous-typage peuvent ensuite être définis en se basant sur la pleine abstraction [246]. Des composants présentant des comportements externes équivalents (ils se comportent de façon identique dans n’importe quel contexte) seront considérés comme équivalents. Un langage est dit modulaire si deux composants ayant une même interface se comportent de façon identique dans chaque contexte possible [159].

Systèmes états transitions et formalismes basés modèle

             La plupart des travaux concernant des approches basés modèle pour la statique combinent Z et des algèbres de processus comme nous avons pu le voir plus haut. Il existe cependant aussi des travaux combinant des systèmes états/transitions avec Z comme µSZ, les machines à configurations ou l’Event Calculus. µSZ. µSZ [60, 59] est un formalisme développé dans le cadre du projet ESPRESS (industrie et instituts de recherche allemands). Il combine Z [184] pour les données (types et opérations) ainsi qu’une forme de Statecharts [140] pour le comportement dynamique et une logique temporelle (logique discrète temporelle d’intervalles) pour exprimer les propriétés de sûreté. Ce formalisme met en avant les propriétés suivantes :
– modularité et réutilisation : composants communicants qui encapsulent leurs données et présentant une interface bien définie. La structure du système est donnée en utilisant les activity-charts [141, 142] ;
– communication et concurrence : communication synchrone à n processus par événements (échange de valeurs par partage de variables) ou par diffusion (par définition de types d’événements et de variables de ces types dans la partie statique), vrai parallélisme et support temporel (événements “tick”) ;
– modèle sémantique sous-jacent permettant de gérer les sorties en fonctions des entrées mais aussi de l’état interne des données (donc plus expressif que les formalismes transformationnels).
La partie Z est étendue par utilisation de rôles : DATA pour l’espace des données (encapsulées) des composants, PORT pour les données partagées constituant l’interface des composants (lecture/écriture), PROPERTY pour un invariant entre variables et INIT pour leur initialisation. Le formalisme prévoit la possibilité d’extension de ces rôles dans le cadre de la méthodologie du projet ESPRESS. Ce Z est étendu à l’aide d’une logique temporelle pour prendre en compte des propriétés de sûreté [61] qui restreint les modèles d’une spécification Z étendu (schémas dynamiques) travaillant au niveau de traces pour les modèles du schéma Z de base. C’est une logique expressive (propriétés d’états, contraintes sur la longueur des traces, contraintes de durées – mais utilisation dans µSZ d’un temps modélisé par événements -, quantification temporelle). Les étiquettes utilisées dans les Statecharts de ce formalisme sont de la forme [garde] evenement / action mais la garde et les actions correspondent à des schémas Z. Il est possible de référer des états de la partie dynamique dans la partie statique (ce qui nuit à la séparation des aspects). L’intégration (opérationnelle) entre aspects se fait par le calcul d’un ensemble maximal de transitions hors conflit (prédicats Z et garde Statechart vrais, états source des Statecharts disjoints). Ces transitions sont effectués en parallèle, et les changements ne sont visibles que dans l’état suivant (atomicité). Le problème qui se pose lorsqu’une même variable peut être modifiée par deux transitions est modélisée par de l’indéterminisme (il faut noter que c’est la valeur dans l’état de départ qui est utilisée). La gestion du temps se fait par événement spécial (“tick”) qui n’est autorisé que si aucun n’autre événement n’est possible. Il est possible de définir des enrichissements dans lesquels deux états du Statechart enrichi et de l’enrichissement de même nom sont identifiés et où deux opérations de la partie statique de même nom sont conjointes. Ce principe permet de définir des comportements plus ou moins abstraits puis de les raffiner. Cet enrichissement n’est toutefois que syntaxique et n’assure par forcement une équivalence (comportementale) quelconque (des conditions pour satisfaire cela ont été définies dans [101]). Ce formalisme dispose de moyens d’animation par codage des schémas Z et utilisation de l’outil Statemate [141]. Un outil de vérification de type est aussi disponible, mais en raison de l’expressivité de ce formalisme, aucune procédure de vérification n’est disponible. Une méthodologie, basée sur les agendas a été définie [133].

Réseaux de Petri de haut niveau

             Les réseaux de Petri (RdP) sont un des formalismes les plus anciens et expressifs. Ils sont aussi très lisibles. Ils permettent l’expression de différents modes de communication (synchrone, asynchrone, causalité entre événements). Des propositions récentes ont été faites pour permettre la structuration (composition parallèle synchrone par fusion de transitions ou de places, asynchrone par réalisation d’un protocole) de RdP, la modularité et la prise en compte d’aspects orientés objets (identité d’objet, création dynamique d’objets et héritage). [33] compare les deux approches consistant à avoir des RdP pour décrire le comportement des objets (ce qui permet la structuration des RdP suivant des concepts objets, et l’expression de concurrence intra-objet) et à avoir des objets dans les RdP (un type de coloration, ce qui est pratique pour la création/destruction dynamique d’instances et la définition de la structure du système) et propose une approche unifiée. Les extensions les plus intéressantes des RdP concernent les RdP de haut niveau [157, 35, 34, 58, 32, 172, 42, 40, 41] (ou colorés, ou algébriques quand il s’agit de termes dont la sémantique est donnée algébriquement) dans lesquels il est possible de prendre en compte la coloration dans des gardes associées aux transitions et d’effectuer des transformations (par exemple algébriques) sur les jetons colorés. La sémantique de tels systèmes est opérationnelle (et nécessite une sémantique initiale pour la partie statique, par exemple OBJ3 pour [35]). Certaines approches permettent l’expression de la vraie concurrence par la définition d’une sémantique de pas. L’approche de [216] est une tentative de fournir un cadre général (théorie des catégories) aux RdP de haut niveau. Il est possible d’effectuer des vérifications sur les RdP toutefois cela s’avère assez complexe. Cela nécessite soit un travail sur les invariants de marquage des places, soit le calcul d’un automate de couverture (pouvant exploser) de façon à utiliser la vérification de modèle. En conclusion, on peut être tenté de dire que d’un point de vue utilisation les RdP restent proches d’UML et sont plutôt adaptés à l’analyse et aux premières phases de la conception. C’est particulièrement le cas de formalismes intégrant les RdP avec d’autres approches ou utilisant les RdP pour combiner plusieurs approches ([132] les utilise par exemple pour combiner automates, programmes parallèles et SDL). Les avantages des RdP par rapport à des formalismes graphiques tels que des systèmes de transitions plus simples et disposant de bons moyens de structuration (produit synchronisé [17] par exemple) concernent essentiellement leur lisibilité et intuitivité. Ils sont outillés [73] et beaucoup utilisés en industrie.

La librairie CLAP

                   Les systèmes à base d’états et de transitions sont un important formalisme de spécification des aspects dynamiques des systèmes. Ils sont aussi au cœur du langage KORRIGAN, c’est pourquoi une partie de la librairie CLIS leur est dédiée. CLAP permet la définition de différents types de systèmes à base d’états et de transitions en fournissant une librairie de classes extensible leur correspondant. Dans l’état actuel de la librairie, il y a ainsi par exemple des classes pour les systèmes avec paramètres d’état (initialité des états, coloration) ou de transition (étiquettes, émissions et réceptions, gardes), ainsi que pour les réseaux de Petri. Il est facile d’ajouter une nouvelle classe correspondant à un nouveau type de diagramme à base d’états et de transitions en sous-classant une ou plusieurs classes existantes. Les diagrammes sont enregistrés dans des fichiers suivant un format interne générique. Un analyseur syntaxique générique pour ce format est disponible. Les diagrammes peuvent être automatiquement transformés en formats d’entrée pour outils graphiques (au choix, XFig ou DOT). Cette fonctionnalité a été réalisée en suivant le principe décrit dans la figure 4.2. La partie originale de cette librairie concerne en fait les systèmes de transition symboliques. Il n’existe en effet actuellement aucun paquetage dédié à ce type de systèmes. Nous n’avons pas pour le moment une implémentation très efficace des STS, mais nous ne pensons pas que l’efficacité soit actuellement le problème le plus important lié à ces systèmes de transition. Les STS sont abstraits et ont donc généralement une taille réduite qui n’impose pas les mêmes besoins en termes d’efficacité que les automates par exemple. Les algorithmes de stockage de graphes habituels sont donc suffisamment efficaces pour l’instant. Une partie de la hiérarchie actuelle de CLAP est présentée dans la figure 4.4. Différents types de systèmes de transitions symboliques sont représentés par les classes GATDiagram et STSKorriganDiagram. La classe GATDiagram décrit les STS généraux avec termes construits à partir de signatures statiques et sans offres, ni émissions ou réceptions. Elle peut être utilisée pour décrire les STS des vues statiques. La classe STSKorriganDiagram est celle utilisée dans le langage KORRIGAN pour les STS des vues dynamiques, elle utilise des termes construits à partir de signatures dynamiques (chapitre 2).

Génération des spécifications LOTOS

                 Chacune des parties dynamiques est modélisée par un processus LOTOS. Nous indiquons aussi la fonctionnalité des processus. Il s’agit ici de processus ne terminant pas ; ils ont donc la fonctionnalité noexit et sont modélisés par des processus récursifs. Chaque processus dispose de données internes (partie type de données des vues) et d’une partie contrôle (partie comportement). Un type est créé pour chaque type de processus et un objet de ce type constitue le paramètre formel du processus (noté p:tp). Ce type devra disposer d’une opération d’initialisation utilisée à l’instanciation du processus. Nous l’appelerons init. Lors de l’instanciation des processus, un appel à l’opération init est substitué au paramètre formel des processus. Enfin, les interactions entre composants sont modélisées par des portes formelles. On peut voir cela comme les services (interface) du composant. Nous donnons maintenant notre méthode semi-automatique d’obtention des spécifications LOTOSà partir de l’automate. Il est possible de procéder de deux façons (voir les schémas de transformation des figures 4.8 et 4.9) : un processus est associé à chaque automate et (i) pour chaque état une branche conditionnelle est créée puis des simplifications sont effectuées afin d’obtenir une spécification plus lisible, ou (ii) un sous-processus est créé pour chaque état de l’automate (cette dernière approche nécessitant/autorisant beaucoup moins de simplifications).

Intégration des parties statiques et dynamiques

                 L’intégration des parties statiques et dynamiques est effectuée en encaspulant une instance de la classe statique dans la classe dynamique, et en effectuant des appels aux méthodes statiques dans les corps des méthodes dynamiques (figure 4.25). Les observateurs sont appelés dans la méthode run de façon à calculer certains des arguments des éléments des listes d’exécution. Les méthodes statiques sont appelées dans chaque méthode dynamique leur correspondant.

Table des matières

Introduction
1 Spécifications formelles mixtes 
1.1 Définitions préliminaires 
1.2 Besoins associés aux spécifications 
1.2.1 Formalité
1.2.2 Expressivité
1.2.3 Abstraction
1.2.4 Lisibilité
1.2.5 Moyens de structuration
1.2.6 Validation et vérification
1.2.7 Méthode
1.2.8 Outillage
1.3 Besoins associés aux spécifications mixtes
1.3.1 Expression des aspects
1.3.2 Cohérence entre aspects
1.3.3 Structuration et réutilisation
1.3.4 Orientation objet
1.3.5 Conclusion sur les besoins
1.4 Panorama des spécifications formelles mixtes 
1.4.1 Approches hétérogènes
1.4.2 Approches homogènes
1.5 Conclusions
2 KORRIGAN et le modèle des vues 
2.1 Le modèle des vues 
2.1.1 Partie données
2.1.2 Partie comportementale
2.1.3 Abstraction
2.1.4 KORRIGAN
2.2 Structuration interne
2.2.1 Aspects statiques
2.2.2 Aspects dynamiques
2.2.3 Autres aspects
2.2.4 Intégration des aspects
2.3 Structuration externe 
2.3.1 Environnements
2.3.2 Formules d’état
2.3.3 Formules de transition
2.3.4 Integration Views
2.3.5 Composition Views
2.4 Structuration d’héritage 
2.5 Sémantique
2.5.1 Obtention d’une structure de vue pour les ESV
2.5.2 Sémantique des ESV
2.6 Conclusions 
3 Méthode de spécification pour systèmes mixtes 
3.1 Motivations 
3.2 État de l’art 
3.2.1 Parties dynamiques
3.2.2 Parties statiques
3.3 Une proposition 
3.3.1 Etape 1 : Description informelle
3.3.2 Etape 2 : Activité concurrente
3.3.3 Etape 3 : Composants séquentiels
3.3.4 Etape 4 : Types de données
3.4 Conclusions 
4 ASK : un Atelier pour Spécifier avec KORRIGAN 
4.1 L’environnement ASK
4.1.1 Principes de conception
4.1.2 Le langage PYTHON
4.1.3 Processus d’intégration
4.2 La librairie CLIS
4.3 La librairie CLAP 
4.4 Outils de l’atelier ASK 
4.4.1 Analyse syntaxique
4.4.2 Opérations pour systèmes de transitions
4.4.3 Traduction, validation et vérification des spécifications
4.4.4 Génération de code concurrent orienté objet
4.5 Traduction des spécifications en LOTOS et SDL 
4.5.1 Génération des spécifications LOTOS
4.5.2 Génération des spécifications SDL
4.6 Génération de code concurrent orienté objet en ActiveJAVA 
4.6.1 Génération de la partie statique
4.6.2 Génération de la partie dynamique
4.7 Conclusions 
Conclusion
Bibliographie
Liste des tableaux

Télécharger le rapport complet