Aller au sommaire principal

ULB - Université libre de Bruxelles

 

AIDE | QUITTER

   

Année académique 2017-2018
24/05/2019
Image transparente

Langue/Language


Formal verification of computer systems
INFO - F412

I. Informations générales
Intitulé de l'unité d'enseignement * Formal verification of computer systems
Langue d'enseignement * Enseigné en anglais
Niveau du cadre de certification * Niveau 7 (2e cycle-MA/MS/MA60)
Discipline * Informatique
Titulaire(s) * [y inclus le coordonnateur] Mickael RANDOUR (coordonnateur), Thierry MASSART, Jean-François RASKIN
II. Place de l'enseignement
Unité(s) d'enseignement co-requise(s) *
Unité(s) d'enseignement pré-requise(s) *
Connaissances et compétences pré-requises * Bonne connaissance de l'algorithmique, de la théorie des langages et de la compilation (exemple : cours INFO090
Programme(s) d'études comprenant l'unité d'enseignement - M-INFOS - Master en sciences informatiques (5 crédits, optionnel)
- M-IRIFS - Master en ingénieur civil en informatique, à finalité spécialisée (5 crédits, optionnel)
III. Objectifs et méthodologies
Contribution de l'unité d'enseignement au profil d'enseignement *
Objectifs de l'unité d'enseignement (et/ou acquis d'apprentissages spécifiques) *

Etude des techniques et outils existants pour spécifier et vérifier formellement des systèmes distribués.

Contenu de l'unité d'enseignement *

- Introduction : notion de spécification et de vérification formelles. - Systèmes à transitions labellées, automates, algèbres de processus, réseaux de Pétri, logiques temporelles. - Propriété de sûreté et de vivacité. - Equivalence de comportement et réductions. - "Model checking", "Refinement checking", test de conformance.

Méthodes d'enseignement et activités d'apprentissages *

Cours ex-cathedra et séminaires de mise en pratique

Support(s) de cours indispensable(s) * Non
Autres supports de cours

Slides du cours

Livres de référence

Références, bibliographie et lectures recommandées *

Clarcke, E., O. Grumberg et D. Peled, 1999. Model Checking. - Mit Press.

IV. Evaluation
Méthode(s) d'évaluation *

Projet avec rapport et présentation généralement à l'exposition du Printemps des Sciences.

Construction de la note (en ce compris, la pondération des notes partielles) *

Oral Exam + project

Langue d'évaluation *

English

V. Organisation pratique
Institution organisatrice * ULB
Faculté gestionnaire * Sciences
Quadrimestre * Deuxième quadrimestre (NRE : 18363, 42269)
Horaire * Deuxième quadrimestre
Volume horaire
VI. Coordination pédagogique
Contact *

Thierry MASSART (Campus Plaine, bâtiment NO, 2N8 113)

Lieu d’enseignement *

Campus Plaine & Solbosch

VII. Autres informations relatives à l’unité d’enseignement
Remarques

Retour aux détails du cursus
Image transparente
Passer directement au début de la page
Version: 8.1.1.17