-
Partager cette page
Formal verification of computer systems
Titulaire(s) du cours
Jean-François RASKIN (Coordonnateur)Crédits ECTS
5
Langue(s) d'enseignement
anglais
Contenu du cours
-
Introduction : notion de spécification et de vérification formelles. - Systèmes à transitions labellées, automates, et logiques temporelles. - Propriété de sûreté et de vivacité. - Equivalence de comportement et réductions. - "Model checking", "Refinement checking", test de conformance. Automates temporisé. Chaines de Markov et processus de décision Markoviens.
Objectifs (et/ou acquis d'apprentissages spécifiques)
Etude des techniques et outils existants pour spécifier et vérifier formellement des systèmes réactifs.
Pré-requis et Co-requis
Cours ayant celui-ci comme co-requis
Méthodes d'enseignement et activités d'apprentissages
Cours ex-cathedra et séminaires de mise en pratique
Références, bibliographie et lectures recommandées
Clarcke, E., O. Grumberg et D. Peled, 1999. Model Checking. - MIT Press.
C. Baier and J.-P. Katoen. Principles of Model Checking, 2008 - MIT Press.
Support(s) de cours
- Université virtuelle
- Syllabus
Autres renseignements
Contacts
Jean-François Raskin (jraskin@ulb.ac.be)
Campus
Plaine
Evaluation
Méthode(s) d'évaluation
- Autre
Autre
Examen oral et projet.
Construction de la note (en ce compris, la pondération des notes partielles)
Examen oral et rapport sur le projet
Langue(s) d'évaluation
- anglais