Sujet :
Conception Formelle en PVS
Responsable : Pierre Castéran
Téléphone : 05 40 00 69 31
e-mail : pierre.casteran@labri.fr
Présentation du sujet :
Il s'agit d'étudier l'adéquation du système PVS (Prototype Verification System)
à la présentation des notions de développement de programmes prouvés et de
raffinement.
PVS est un système pour la vérification de logiciel en open-source, comportant un prouveur semi-automatique. Ses applications principales sont la vérification de matériel, de protocoles, et de systèmes critiques.
Par ailleurs, il a été développé un outil appelé PBS, écrit en Ocaml, permettant de traduire les machines abstraites de B en théorie PVS.
Travail à faire :
Il consistera à :
- S'initier à la technologie PVS (un très bon tutorial peut être chargé depuis le site sus-mentionné, et PVS est enseigné à l'ENSEIRB, suivre ce lien )
- Comprendre comment PVS permet de modéliser le concept de machine abstraite
et de raffinmenent,
- Tester PBS, et résoudre en PVS les obligations de preuves engendrées par cet outil.
- Les exemples de machines abstraites et de raffinements seront ceux vus en
cours
Mot-clés : Conception formelle, Preuves, Logiciel libre.