Modélisation logique et formalisation des systèmes

NIVEAU

Électif 2A / Séquence thématique 3A

ACTEURS

• Frédéric Boulanger
• Safouan Taha
• Benoît Valiron
• Idir Aït Sadoune
• Lina Ye ?
• ?

RÉSUMÉ

De plus en plus de systèmes embarqués et systèmes critiques en général sont maintenant analysés à l'aune des méthodes formelles. Basées sur la logique et issues de plus de 50 ans de recherches en informatique théorique, ces méthodes permettent de modéliser formellement un système donné, afin de pouvoir spécifier, raisonner sur, et ultimement prouver des propriétés de sureté et de fonctionnement. La modélisation logique permet également de résoudre des problèmes exprimés sous la forme d'un ensemble de contraintes à satisfaire.

L'objectif de cette séquence thématique/électif est d'introduire la problématique de la modélisation logique et de la formalisation des systèmes, et de présenter quelques outils sur des problèmes concrets.

MÉTHODE D'ENSEIGNEMENT

Les notions théoriques seront présentées en cours, mais une grande part de l'enseignement se fera sous forme de bureaux d'étude sur machine, et de mini-projets débutés lors d'études de laboratoire.

THÈMES ABORDÉS

• Logique du premier ordre, logiques d'ordre supérieur
• Programmation fonctionnelle, lambda calcul, typage
• Déduction naturelle, règles d'inférence, introduction/élimination
• Spécifications, théories, modèles
• Systèmes de transitions
• Logique de Hoare
• Raffinement de modèles

OUTILS UTILISÉS

• Model checking (Alloy) : formalisation et exploration de modèles discrets
• Solveurs SMT / SAT ?
• Why3 : Semi-automatisation de preuves de programmes
• Rodin/Event-B : Outil supportant une méthode formelle basée sur le raffinement et la preuve
• Isabelle : outil générique de preuves formelles.