DEA d'informatique de l'université de Rennes 1

Filière 2 : «génie logiciel et méthodes formelles»

Module A2R

« analyse, synthèse et supervision des systèmes réactifs et répartis »

Cette page est tenue à jour à l'adresse suivante : http://www.irisa.fr/s4/dea/a2r/index.html

 

Ce module est en deux parties enseignées alternativement une année sur deux. Une partie porte sur l'analyse et la supervision de réseaux de Petri , et l'autre sur sur les méthodes formelles pour la vérification des systèmes réactifs . Vous pouvez consulter le calendrier de l'année en cours.

Partie Méthodes Formelles pour la Vérification des Systèmes Réactifs

  • Intervenant :
  • Sophie Pinchinat, maître de conférences à l'université de Rennes 1(Sophie.Pinchinat@irisa.fr, bureau C202, tél. 0299847254).
  • Volume : 21 heures
  • Présentation

    • De nos jours, l'omniprésence de l'informatique dans les réseaux de communication et la manière dont les programmes se substituent à l'homme pour des tâches délicates (e.g. contrôle d'appareils d'assistance médicale, régulation thermique de réacteurs nucléaires, etc...) imposent le développement de méthodes rigoureuses et efficaces pour la validation des produits logiciels. Les systèmes qui nous occupent dans ce contexte sortent du champ des programmes dits transformationnels : ils n'ont pas forcément d'état final, et notre intérêt porte plutôt sur leur comportement réactif. C'est dans ce sens que Pnueli les appelle systèmes réactifs .

    Les méthodes formelles définissent des techniques d'analyse des systèmes réactifs qui se situent en amont de méthodes bien connues de simulation et de test. Elles s'appuient sur des théories mathématiques permettant de construire les systèmes - on parle de spécification et de synthèse -, d'exprimer leurs propriétés et de raisonner de façon rigoureuse sur leur comportement - on parle encore de spécification et de vérification -, et, dans l'éventualité de mettre au point ses systèmes par exemple en les contrôlant, - on parle du contrôle d'un système -. Dans ce cours nous proposons une exploration de certaines de ces méthodes.

  • Plan du cours
  • Bibliographie

    1. Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie, and A. Petit. Vérification de logiciels : Techniques et outils du model-checking. Vuibert, 1999.

    2. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.

    3. E. M. Clarke, Orna Grumberg, Doron Peled . Model Checking Mit 314 pages (December 1999)

    4. E. A. Emerson, Temporal and modal logic. In J. van Leeuwen, editor, "Handbook of Theoretical Computer Science, vol B ", chapter~16, pages 995--1072. Elsevier Science Publishers, 1990.

    5. E. A. Emerson, Automated Temporal Reasoning about Reactive Systems. Logics for Concurrency: Structure versus Automata, F. Moller and G. Birtwistle (eds.), Springer LNCS no. 1043, Pages 111-120.

    6. Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM , 47(2):312--360, March 2000..

    7. Automata, Logics, and Infinite Games: A Guide to Current Research. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors.. [Outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002. http://www-mgi.informatik.rwth-aachen.de/Misc/LNCS2500/

    8. André Arnold, Aymeric. Vincent, Igor Walukiewicz: Games for synthesis of controllers with partial observation. TCS 1(303): 7-34 (2003)

    9. Igor Walukiewicz. Automata and logic. In Notes from European Educational Forum Summer School'01, 2001.

    Partie analyse et la supervision de réseaux de Petri

  • Intervenant :
  • Benoît Caillaud, chargé de recherche à l'INRIA (Benoît.Caillaud@irisa.fr, bureau C201, tél. 0299847407)
  • Volume : 18 heures
  • Présentation

    • Ce module est une initiation aux techniques indispensables à l'analyse, la synthèse et le contrôle des logiciels (ou systèmes) réactifs et répartis : protocoles dans les réseaux de télécommunication, systèmes d'information répartis, systèmes de commande embarqués, etc. Il commence par des éléments de la théorie des réseaux de Petri (un modèle de la concurrence universel et polyvalent) pour ensuite aborder les techniques et l'algorithmique de la vérification de propriétés de sûreté et de vivacité des réseaux de Petri. Ensuite, seront développés la théorie des régions et les algorithmes de synthèse de réseaux qui en découlent. Ce module s'achèvera sur une introduction au contrôle de supervision, dans les cas particuliers des réseaux de Petri et du contrôle décentralisé.

  • Plan du cours
  • Bibliographie

    1. T. Murata, Petri Nets: Properties, Analysis and Applications, "Proceedings of the IEEE", 1989, vol. 77, no. 4, pp 541-580.

    2. M. Silva, E. Teruel, J. M. Colom, Linear Algebraic and Linear Programming Techniques for the Analysis of Place/Transition Net Systems, "Lectures on Petri nets I : basic models, advances in Petri nets", LNCS, vol. 1491, Springer, 1999, pp. 309-373.

    3. A.Giua, C. Seatzu, "Design of observers/controllers for discrete event systems using Petri nets," in Synthesis and Control of Discrete Event Systems, B. Caillaud, X. Xie, Ph. Darondeau and L. Lavagno (Eds.), pp. 167-182, Kluwer, 2001.

    4. E. Badouel, P. Darondeau. Theory of regions. in Lectures on Petri Nets I: Basic Models, pages 529-586, Springer, Lecture Notes in Computer Science, Volume 1491, 1999.

    5. J. Esparza, S. Roemer. An unfolding algorithm for synchronous products of transition systems. in "CONCUR'99 Concurrency Theory, 10th International Conference", LNCS, vol. 1664, pp. 2-20, Springer, 1999.

  • Calendrier