A2R : analyse, synthèse et supervision des systèmes réactifs et répartis

• Intervenants : Sophie Pinchinat, maître de conférences à l'Ifsic (Sophie.Pinchinat@irisa.fr)
• Volume : 21 heures
• Equipe de recherche : S4

Présentation

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 les méthodes formelles pour la vérification des systèmes réactifs. Cette année le module qui vous est proposé est:

Méthodes Formelles pour la Vérification des Systèmes Réactifs
proposée par Sophie Pinchinat.

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 -.

Plan du module 

Cours 1	Introduction à la vérification des systèmes.
Cours 2	Représentation des systèmes
Cours 3	Logiques temporelles et modales.
Cours 4	Model Checking par méthodes itératives.
Cours 5	Méthodes formelles par automates d'arbres
Cours 6	Procédures de décision basées sur les jeux de parité.
Cours 7	Vers les problèmes de synthèse de contrôleurs.

 

Bibliographie

• Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie, and A. Petit. Vérification de logiciels : Techniques et outils du model-checking. Vuibert, 1999, mais aussi 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.*
• E. M. Clarke, Orna Grumberg, Doron Peled . Model Checking Mit 314 pages (December 1999)
• 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.
• 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.
• 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.
• 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/.