Journées FAC'2002
26 et 27 mars 2002
LAAS-CNRS - Toulouse

Formalisation des Activités Concurrentes Dixième Edition

Organisées par le groupe SVF / FéR IA : Spécification, Vérification Formelles.

---

Francois Terrier       CEA-LIST

          UML, de la programmation à la modélisation :
               vers le développement basé sur les modèles des systèmes embarqués

transparents     résumé   Porté par l'intérêt pour l'orienté objet, UML apparaît comme un standard de fait pour la modélisation des systèmes du futur. En dehors de son caractère de norme qui lui assure une certaine stabilité, ce standard offre suffisamment de flexibilité pour être adapté à divers domaines techniques. C'est d'ailleurs, en grande partie l'introduction formelle et normalisée de processus d'adaptation de ce langage qui en assure le succès. Dans ce contexte, son emploi pour le développement de systèmes temps réel à mené à des propositions industrielles relativement variées comme ARTiSAN, RT-UML/Rhapsody, UML/SDL, UML-RT/Rose ou SyncChart-Esterel. Toutefois, ces approches restent très dépendantes d'un modèle d'exécution et de choix de mise en oeuvre lié à l'offre et à la stratégie commerciale des outils. Pour gérer cette variabilité des choix de mise en oeuvre, la réflexion s'oriente de plus en plus vers la mise en place d'une méthodologie de développement basée sur les modèles (Model Driven Architecture) qui est maintenant le nouvel objectif que s'est fixé l'OMG. Cette approche trouve un écho particulier dans le domaine des systèmes embarqués, précisément pour aider à structurer la démarche de développement en sous-ensembles de modèles et augmenter l'indépendance entre modèles fonctionnels, modèles d'exécutions et architectures matérielles.

Papier/Transparents - à venir

papier      résumé   Le développement des systèmes complexes nécessite la mise en ouvre de méthodologies permettant d'assurer une maîtrise de la qualité du système construit, ainsi que la possibilité de faire coopérer des techniques formelles, contribuant à l'amélioration des systèmes. Dans cet article nous présentons une méthodologie fondée sur la notion de composant, permettant la conception et la validation incrémentale d'un système. Nous présentons ensuite une traduction des notions de composant et de composition dans la technique formelle associée au langage LUSTRE à travers une étude de cas issue du domaine de l'avionique modulaire intégrée (AMI).

transparents      papier      résumé    Depuis quelques années, l'attention s'est portée sur le niveau organisationnel des Systèmes Multi-Agents et notamment sur les protocoles qui permettent aux agents d'interagir. La définition et l'implantation d'un protocole mettent en jeux un grand nombre de mécanismes et de propriétés qui concernent non seulement le protocole lui-même, mais aussi les entités en interaction et leurs l'environnements d'exécution, les media de communication et les mécanismes de régulation qui peuvent exister au niveau de l'ensemble du système. L'ensemble de ces éléments déterminent ce que l'on pourrait appeler un espace d'interaction, et donc les caractéristiques des protocoles que l'on peut déployer dans un système. Cet article se propose d'établir un inventaire de ces éléments en les répartissant en quatre niveaux, ce qui pourrait déboucher sur une typologie des espaces d'interaction.

transparents      papier     résumé    Notre objectif est la vérification d'algorithmes génériques de tolérance aux fautes. Nous souhaitons améliorer le processus de test en utilisant des informations extraites des preuves, formelles ou informelles, de l'algorithme. À titre d'exemple, nous étudions l'algorithme d'ordonnancement FT-RMS (Fault-Tolerant Rate Monotonic Scheduling), prouvé par une démonstration informelle, et révélé incorrect par la suite. Nous nous attachons à l'analyse de sa preuve informelle, que nous restructurons sous la forme d'un arbre de preuve semi-formel, dont sont extraits plusieurs cas fonctionnels utilisés pour tester un prototype de l'agorithme. Les résultats expérimentaux montrent qu'une preuve informelle fausse peut ne pas apporter d'informations pertinentes pour le test. Il nous reste à étudier si une preuve formelle partielle nous pemettrait d'établir une meilleure connection avec les fautes.

transparents      papier      résumé   L'objectif de cet exposé est de présenter une étude de cas, du domaine avionique, pour les techniques de vérification formelle de propriétés temporelles ou temporisées. Cette étude de cas, proposée par Dassault-Aviation, est une simplification du système de contrôle des trains d'atterrissage d'un avion du type Rafale. Ce système est composé de trois trains différents, qu'il s'agit de commander en fonction des ordres du pilote (ordre de descente ou de remontée des trains) au moyen d'un ensemble d'actionneur (électrovannes, contacteurs?). Ce système est bien entendu soumis à des exigences telle que : " l'ordre de remontée des trains alors que l'avion est au sol ne doit pas être exécuté "? Ce système a été programmé en Esterel par Dassault Aviation. Or, du fait de la présence de nombreux " timers " au sein du système, les outils de " model checking " propres aux langages synchrones échouent dans la vérification du système. L'objectif de cette présentation est d'exposer les raisons de cet échec, et de proposer un " challenge " aux équipes de recherche du domaine, à savoir la vérification d'une propriété définie ci-après sur l'étude de cas complète.

transparents      papier      résumé    Ce papier présente un cadre basé sur les Réseaux de Petri Stochastiques (RdPS) pour l'analyse de la Qualité de Service (QdS) dans les réseaux à commutation de paquets. Nous y présentons les modèles RdPS des principaux algorithmes qu'implémentent les mécanismes de mise en forme et mise en vigueur de trafic, de gestion de buffer, et d'ordonnancement de paquets ; une méthode permettant de construire le modèle d'un réseau avec une architecture quelconque ; ainsi qu'une méthode d'analyse permettant de mesurer les principaux métriques de QdS, à savoir : le taux de pertes de paquets associé à un flux, le délai moyen de transfert des paquets d'un flux, des bornes supérieures et inférieures sur le délai de transfert des paquets d'un flux, l'utilisation de la bande passante d'une ligne, etc.

papier      résumé   Dans le cadre de la modélisation des systèmes réactifs, des logiques temporelles ont été développées au cours des années 80. Ces logiques permettent d'exprimer des contraintes qualitatives entre les événements telles que "Le système sera stoppé après que quelqu'un a appuyé sur le bouton d'arrêt d'urgence." mais ne permettent pas d'exprimer des contraintes quantitatives telles que "Si quelqu'un appuie sur le bouton d'arrêt d'urgence alors le système sera stoppé dans les cinq secondes qui suivent." La nécessité de pouvoir exprimer de telles informations a amené à développer des logiques dites "temps-réel" (généralement des extensions de logiques temporelles existantes), à partir de la seconde moitié des années 80. C'est parmi ces logiques que se situe le calcul des durées dont la particularité est de permettre d'exprimer la durée pendant laquelle un système se trouve dans un état donné, au cours d'un intervalle de temps. Plusieurs types de problèmes peuvent être étudiés, telles la vérification de modèle qui consiste à vérifier si un modèle donné satisfait une formule donnée et la satisfaisabilité qui consiste à chercher si une formule donnée est satisfaite dans au moins un modèle. Nous nous sommes intéressée au problème de la satisfaisabilité pour un fragment du calcul des durées pour lequel nous avons développé une méthode de décision basée sur la méthode des tableaux. Cette méthode consiste à tout d'abord bâtir un arbre étiqueté (appelé "tableau") à partir d'une formule dont on cherche à savoir si elle est satisfaisable. Puis si l'une des feuilles du tableau possède certaines propriétés de cohérence, il est alors possible de construire un modèle de la formule d'origine, qui est ainsi satisfaisable. Dans le cas contraire la formule n'est pas satisfaisable. Nous avons montré que la méthode développée est correcte, complète et termine.

Hubert Garavel       INRIA/VASY

          Panorama des outils CADP

transparents     résumé   CADP (Caesar/Aldébaran Development Package) est une boîte à outils pour le développement des systèmes asynchrones qui offre des fonctionnalités multiples : simulation, génération de code, génération de tests, vérification basée sur des logiques temporelles et des bisimulations, vérification compositionnelle, etc. Dans cet exposé, nous présentons les principes et l'architecture de CADP et nous faisons le point sur les récentes avancées et les futures directions de recherche.

Papier/Transparents - à venir

transparents      papier     résumé   Cet article présente une algèbre de processus temporisés appelée TPAPa et une extension de celle-ci, TPAPas. Le but de ces algèbres est de modéliser un ensemble de processus embarqués se partageant des ressources communes et sensibles aux délais de communication et aux stratégies de séquencement. La communication par diffusion temporisée et la suspension sans reprise (abort) sont les notions fon- damentales de TPAPa. Elles permettent la définition de séquenceurs et de médiums de communication asynchrones qui seront pris en compte lors de la vérification du comportement temps-réel du système. Après avoir définis les caractéristiques de l'algèbre TPAPa, une étude de cas du domaine avionique est modélisée à l'aide de TPAPa puis vérifiée à l'aide du model checker UPPAAL. Une amélioration de TPAPa par un opérateur de suspension de processus avec reprise est ensuite proposée et formalisée dans l'algèbre TPAPas. Les processus de TPAPas sont équivalents à des automates non plus temporisés mais hybrides et ne peuvent donc plus être vérifiés à l'aide de model checker tels que UPPAAL.

transparents      papier     résumé    Le propos de cet article est de montrer que l'utilisation conjointe des réseaux de Petri p-temporel, des graphes AOA et des TCSP nous permettent de trouver au moins une solution satisfaisante à un problème d'ordonnancement en temps contraint pour chaque ordre partiel sans avoir à construire le graphe de tous les états possibles de notre modèle. Nous présenterons comment la logique linéaire nous permet de générer un ordre partiel vérifiant les contraintes logiques sans avoir à construire tout le graphe d'état. Un cas d'étude de présentation de document interactif multimedia sera utilisé pour bien montré la méthode utilisée afin de trouver une solution d'ordonnancement cohérente.

P.O Ribet, F. Vernadat, B. Berthomieu - LAAS/CNRS

transparents      papier      résumé   Une approche commune à la vérification des systèmes concurrents consiste à construire le graphe des états accessibles représentant de façon exhaustive le comportement du système et à l'analyer. Malheureusement, ce graphe d'états est souvent trop grand pour être effectivement construit: sa taille évolue le plus souvent de façon exponentielle en le nombre de composants du système. Pour limiter cette explosion, des techniques d'exploration partielle ont été développées permettant d'obtenir des graphes d'états réduits qui offrent les mêmes capacités d'analyse. Les techniques d'ordre partiel ont été développées pour limiter l'explosion combinatoire en s'attaquant à l'une de ses causes la représentation du parallélisme par l'entrelacement d'actions. Ce papier étudie la coopération de deux de ces approches: les explorations partielles basées sur les ensembles "persistants" et les "graphes de pas couvrants". Un algorithme général d'exploration partielle combinant ces deux approches et en cumulant les bénéfices est proposé.

transparents      papier     résumé   Erlang est un langage fonctionnel non typé concurrent et distribué conçu par ERICSSON pour la programmation de leurs équipements de télécommunication. Il hérite de nombreux concepts de Prolog et de LISP et intègre des mécanismes sophistiqués pour la programmation d'applications distribuées. L'absence de mécanisme de typage, c'est-à-dire de vérification statique de certaines formes de correction de programmes, complique la tâche des programmeurs. Nous présentons dans cet article les travaux que nous menons pour munir Erlang d'un système de type. Celui-ci est dérivé de travaux précédents réalisés dans le cadre des acteurs. Ils ont permis la mis au point d'un prototype de système de type pour Erlang. Celui-ci consiste en l'inférence d'un type pour chaque programme et en la vérification de la correction de ce programme par la résolution des contraintes collectées par le système d'inférence.

transparents      papier     résumé   Un calcul réparti d'agents mobiles pose de nouveaux problèmes de contrôle et de mise au point des applications réparties. Ceux-ci touchent aussi bien la sécurité (par la migration de code) que la supervision globale ou le mode d'exécution (déconnecté par exemple). Nous envisageons ici plus particulièrement le problème du rejeu d'un tel calcul.
Pour ce faire, nous utilisons une modélisation d'un calcul d'agents mobiles fondée sur la notion de chemins répartis. Chaque chemin est une abstraction du parcours d'un agent de sites en sites. La structure du calcul en terme de chemins est représentée par des vecteurs de chemins. Tout chemin parcouru par un agent peut être représenté par une suite de tels vecteurs. Mais, propriété intéressante, il suffit de connaître le dernier vecteur de chaque chemin pour d'une part détecter la terminaison du calcul et d'autre part reconstruire tout le graphe causal du calcul réparti. Cette dernière propriété est la plus importante puisqu'à partir de ce graphe il sera possible de rejouer le calcul de façon déterministe en respectant l'ordre de visite des agents sur chaque site levant ainsi tout non déterminisme dû aux échanges de messages (sous-jacents aux migrations).