Centre Fédéré en Vérification






Seminars for 2004-2005

  • Model Checker Aided Design of a Controller for a Wafer Scanner
    • Speaker: Frits Vaandrager, Nijmegen Institute for Computing and Information Sciences
    • Date: November 12th, 2004
    • Abstract:
    • I intend to present an overview of some recent work that has has been carried out within the EU IST project AMETIST, in which timed automata technology is applied to solving various scheduling problems.

      One case study that I will discuss in more detail was carried out together with Martijn Hendriks (Nijmegen) and Barend van den Nieuwelaar (ASML/TUE). For a design of a new wafer scanner for the semiconductor industry, we show how model checking techniques can be used to compute (i) a simple yet optimal deadlock avoidance policy, and (ii) an infinite schedule that optimizes throughput. Deadlock avoidance is studied based on a simple finite state model using SMV, and for throughput analysis a more detailed timed automaton model has been constructed and analyzed using the UPPAAL tool. The SMV and UPPAAL models are formally related through the notion of a stuttering bisimulation. The results were obtained within two weeks, which confirms once more that model checking techniques may help to improve the design process of realistic, industrial systems. Methodologically, the case study is interesting since two models (and in fact also two model checkers) were used to obtain results that could not have been obtained using only a single model (tool).

  • Quelques problèmes dans l'arithmétique de Presburger et l'arithmétique de Skolem.
    • Speaker: Denis Lugiez, Université de Provence (U1) Marseille (FRANCE)
    • Date: March, 4th, 2005
    • Venue: Auditorium H, Forum building, Campus Plaine
    • Abstract:
    • L'étude des nombres est un des domaines les plus ancien des mathématiques et a suscité la curiosité des mathématiciens depuis les temps les plus reculés. Depuis les travaux des logiciens du siècle précédent on sait qu'il est vain de vouloir tout connaitre de l'arithmétique dans laquelle on autorise la multiplication et l'addition. Mais ces logiciens ont aussi montré rapidement que si on n'utilise que l'addition (arithmétique de Presburger) ou que la multiplication (arithmétique de Skolem) alors on obtient des théories décidables. Ensuite l'informatique est arrivée, et on s'est aperçu que ces théories logiques qui semblaient n'etre que des objets logiques intéressants mais uniquement théoriques étaient très utiles pour plusieurs applications de cette discipline, en particulier pour l'étude formelle de systèmes informatiques ou modelisés par des sytèmes informatiques, domaine en plein developpement actuellement. On ne compte plus les systèmes de preuve automatiques ou semi-automatiques qui utilisent une procédure de décision de l'arithmétique de Presburger (reposant sur l'élimination de quantificateur ou des méthodes d'automates en général).

      Cela relance l'intéret sur l'étude de ces théories et alors que le domaine semblait bien connu, on s'aperçoit que certains problèmes méritent d'être repris et que des questions intéressantes restent encore sans réponse satisfaisante. Le premier sujet que j'aborderai dans cet exposé concerne les différentes représentations des solutions d'une formule de l'arithmétique de Presburger. Celles-ci peuvent etre représentées par la formule (après élimination des quantificateurs par exemple), mais ausi par un ensemble semi-linéaire ou encore par un automate qui reconnait les représentations binaires des tuples de solutions. Chaque formalisme a des avantages et des inconvénients selon les calculs qu'on veut effectuer, et il est donc intéressant de passer efficacement de l'un à l'autre (si cela est possible). Le formalisme automate permet de représenter plus d'ensembles et caractériser les automates qui correspondent à l'arithmétique de Presburger est un résultat difficile du à Semenov. Muchnik en donne une preuve accessible mais sa méthode reste encore inutilisable en pratique. Je rappelerai les résultats obtenus par Latour et Leroux pour le calcul d'une formule à partir d'un automate et je présenterai les résultats que j'ai obtenus pour passer d'un automate à la forme semilinéaire pour certains types d'ensembles et des résultats (ou questions) sur la complexité des représentations. Je terminerai en donnant quelques indications sur les résultats récents de Leroux pour le passage automate vers formules.

      Ensuite je parlerai du parent pauvre, l'arithmétique de Skolem, en rappelant rapidement quelques résultats de base sur cette théorie et je montrerai comment elle peut être utilisée pour prouver des résultats de décidabilité sur une théorie de multi-ensembles équipée d'opération(s) de comptage.

  • Contrôle de systèmes distribués.
    • Speaker: Paul Gastin, LSV Cachan (France)
    • Date: April, 15th, 2005
    • Venue: Auditorium F, Forum building, Campus Plaine
    • Abstract:
    • Dans la panoplie des méthodes formelles utilisées pour assurer la sécurité des systèmes informatiques, la synthèse de contrôleurs constitue une approche particulièrement intéressante. Dans ce cadre, on suppose donnés d'une part un modèle de système ouvert (atelier de production, ...) dont les actions peuvent être soit contrôlables par programme soit incontrôlables (environnement) et d'autre part une spécification décrivant l'ensemble des comportements souhaitables. L'objectif est de synthétiser, si cela est possible, un contrôleur agissant uniquement sur les actions contrôlables de telle sorte qu'indépendamment des actions de l'environnement, les comportements du système restent corrects. Ce problème a été largement étudié dans le cadre séquentiel des systèmes à événements discrets depuis les travaux fondateurs de Ramadge et Wonham. Dans tous les cas raisonnables, on peut décider si le système est contrôlable et, si oui, synthétiser un contrôleur. L'intérêt principal de la synthèse de contrôleur est que l'on obtient des systèmes sûrs par construction, il est donc inutile de les vérifier ensuite.

      La plupart des systèmes complexes aujourd'hui présentent des aspects distribués. Les processeurs exécutent plusieurs tâches simultanément, ils coopèrent et communiquent par échange de messages au travers de réseaux, ils doivent réagir aux stimuli d'un environnement, etc. De tels systèmes informatiques contrôlent des éléments critiques (centrales nucléaires, réseau ferré, ...) ou sont embarqués pour rendre des services cruciaux dans des véhicules, des cartes à puces, des téléphones, etc. Le problème du contrôle se pose donc très naturellement dans le cadre des systèmes distribués. La difficulté supplémentaire est liée au fait que les contrôleurs doivent être locaux aux composants du système et n'ont qu'une connaissance partielle des comportements puisqu'ils ne peuvent observer que localement ce qui se passe sur leur composant.

      Les premiers travaux de Pnueli et Rosner sur le contrôle distribué étaient motivés par la synthèse de programmes pour les circuits. Ils ont naturellement considéré des systèmes totalement synchrones et ont montré que même pour des spécifications simples (LTL) le problème du contrôle est indécidable pour presque toutes les architectures de circuits. Les architectures décidables sont essentiellement de type "pipeline". Ces résultats ont été généralisés par Kupferman et Vardi pour des spécifications CTL^* et pour le mu-calcul et par Madhusudan et Thiagarajan pour des spécifications locales.

      Les problèmes de contrôle sont souvent décrits et résolus en utilisant des jeux dans lesquels un joueur représente le contrôleur et son adversaire est l'environnement. Dans le cadre distribué, on considère plusieurs joueurs (les contrôleurs locaux) et un environnement. Il s'agit de jeux à information partielle puisqu'à nouveau la stratégie d'un joueur ne doit dépendre que de ce qu'il a pu observer localement. Mohalik et Walukiewicz ont utilisé cette approche dans le cadre du contrôle distribué, obtenant grâce à deux techniques de réduction tous les cas décidables précédents.

      Avec Lerman et Zeitoun, j'ai reconsidéré le problème du contrôle distribué en changeant quelques hypothèses. D'une part, nous nous plaçons dans un cadre asynchrone et nous considérons des spécifications correspondant à des reconnaissables de traces de Mazurkiewicz. D'autre part, nous autorisons les contrôleurs à utiliser une mémoire causale plutôt qu'une mémoire purement locale. Cette mémoire causale, qui permet à un joueur de baser sa stratégie sur tout son passé causal, peut être implantée sur l'architecture considérée simplement en surchargeant les messages échangés dans l'exécution normale du système. Nous avons montré que sous ces hypothèses, le problème du contrôle distribué est décidable pour toutes les architectures série-parallèles et toutes les spécifications reconnaissables. Ce résultat positif contraste fortement avec les résultats essentiellement négatifs précédents.

  • Decidable and undecidable problems in decentralized observation and control
    • Speaker: Stavros Tripakis (CNRS, Verimag)
    • Date: May, 20th, 2005
    • Abstract:
    • The problems of checking existence of and synthesizing (when they exist) observers and controllers are essentially closed in the centralized case, that is, the case of a single observer/controller for the entire plant. The situation is much less clear in the decentralized case. One thing is certain, however: undecidability is common in decentralized settings.

      In this talk I will try to give an overview of what I believe are key facts in decentralized observation and control. I will present both decidable and undecidable problems (including old results such as [Pnueli-Rosner 1991], and newer results in the discrete-event system framework) in an attempt to identify the limits of (un)decidability.

Follow these links to access the lists of 2002-2003 and 2003-2004 seminars.

Links to other seminars




Wed Apr 20 11:11:13 CEST 2005