Formalismes de Description des Systèmes (FDS) 6 ECTS Parcours : GL_Sdf, GL_Verif, AMF_Verif Semestre : S3 Responsables : Anca Muscholl et Emmanuel Fleury Prérequis : notions élémentaires de modèles de calcul et automates Objectifs : La plupart des systèmes informatiques complexes, qu'ils soient matériels ou logiciels, présentent aujourd'hui des aspects distribués et/ou continus. Concevoir de tels systèmes complexes à l'aide de méthodes formelles est crucial pour assurer la sûreté d'un nombre toujours croissant de systèmes critiques. Ce cours décrit des modèles et des formalismes de spécification qui sont capables de représenter des caractéristiques comportementales variées. Programme : * Systèmes discrets : - systèmes de transition, produit de synchronisation - réseaux de Petri - diagrammes de séquence, automates communicants - algèbres de processus - langages de haut niveau (Esterel, Lustre, ...) - automates à contraintes * Systèmes continus : - automates temporisés - automates hybrides - outils tels que Spin, Hytech, Uppaal, Kronos Bibliographie : E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000. Ph. Schnoebelen (coord.) Vérification de logiciels. Vuibert, 1999. A. Arnold. Finite transition systems, Prentice-Hall. 1994. Controle des connaissances : - examen écrit de 3h00 (2/3), - controle continu (1/3)