Systèmes Temporisés, Spécifications Et Vérifications : Optimisation Du Coût De La Vérification

Résumé: Afin de spécifier et de vérifier les systèmes temporisés ; systèmes distribués temps réel, nous avons étudié deux formalismes puissants que sont :"Les automates temporisés introduits par R.Alur et D.Dill "L'algèbre des processus temporisés ATP par J.Sifakis et X.Nicollin . Ceux-ci étant inhérents du fait que l'on peut traduire une expression algébrique ATP en un graphe temporisé ; c'est la compilation ATP ' graphes temporisés. Avec une introduction aux systèmes de transitions étiquetés, introduits par André Arnold et à l'algèbre des processus communicants ACP introduite par Bergstra et Klop ;Ces derniers étant encore dépourvus de la notion du temps et de délais, qui s'imposent actuellement dans les systèmes distribués temps réel ou temporisés ( ex des systèmes embarqués ,protocoles de communication, services Web, monitoring system, circuits logiques ?) Le problème fondamental qui se pose, pour les automates temporisés et leur représentation en mémoire est l'explosion combinatoire lorsqu'il s'agit de cas réels.En effet le nombre de configuration possibles d'un système temporisé, celui-ci étant obtenu par l'opération de composition parallèle || des ses composants, tend vers l'infini en plus du fait que le domaine temporel choisi est dense. Afin de réduire cette explosion, nous opérons sur un automate des régions - au lieu de l'automate lui-même- obtenu par une relation d'équivalence sur l'ensemble des contraintes temporelles. Ainsi les opérations de vérification (model-checking) peuvent s'opérer sur le graphe des régions construit, et considéré comme un automate classique. Dans notre travail, nous avons proposé une méthode permettant d'optimiser le coût de la vérification (model checking) en opérant sur les constantes figurant dans les contraintes temporelles des variables horloges, avec des conséquences sur le nombre des régions, le graphe des régions et les séquences d'exécution.De même que les automates temporisés permettent d'exprimer les contraintes temporelles, nous avons étudié l'algèbre des processus temporisés ATP (extension de ACP) disposant des opérateurs temporels qui permettent d'exprimer les délais tels que :"Les watchdogs "Timeout Pour la vérification des propriétés,(vivacité ,sûreté , réponse bornée) nous avons considéré la logique temporelle TCTL , extension de CTL (Clark et Emerson) ,langage formel défini par une grammaire et qui donne lieu à des algorithmes de model-checking (et symbolique) et de fait automatisables.Nous avons obtenu la licence du package CADP Construction and Analysis of Distributed Processes", d'Hubert Garavel des laboratoires VASY et Verimag del'INRIA Sophia Antipolis , Nous l'avons installé on line et sommes en phase de configuration des variables d'environnements version Win32. Ce package inclut entre autres les outils "Aldebaran : minimisation et comparaison des systèmes de transition,"Bcg_edit : éditeur de graphes "EVALUATOR :model-checkers pour logique temporelle"CEASAR : compilation Lotos ' automate d'état finis Et peut être extensible par l'apport d'outils tels que : "compilation ATP ' automate temporisé, "optimisation par la communauté des licenciés CADP , dont nous faisons partie, ce qui pourrait être perçu comme perspective à notre travail.

Publié dans la revue: