Développement de logiciels critiques avec l'assistant Coq

Dans les domaines informatiques critiques (code embarqué, protocoles, e-commerce), il est nécessaire de pouvoir accorder un haut niveau de confiance dans le code des logiciels utilisés. Les critères communs jalonnent ces niveaux de confiance en 7 échelons.

Le premier niveau est atteint si les fonctionnalités du logiciel ont été testées. Pour atteindre le plus haut niveau de certification de logiciel, il faut pouvoir prouver que le code logiciel produit respecte bien sa spécification.

Dans ce contexte, nous appuierons notre démarche sur l'outil Coq développé à l'Inria et distribué librement (http://coq.inria.fr).

Objectifs

- comprendre les mécanismes de preuves formelles mis en ?uvre dans la production de code pour les logiciels critiques pour lesquels le zéro défaut est crucial

- acquérir l'autonomie nécessaire pour faire des preuves de logiciels critiques à l?aide de l'outil Coq et extraire du code Ocaml certifié.

Public concerné

Ingénieurs et techniciens supérieurs

Connaissances requises

Maîtrise d'un langage de programmation

Méthodes pédagogiques

- conférences illustrées par de petits exemples traités sur ordinateur par les participants pour démystifier le domaine de la preuve assistée par ordinateur

- étude de cas plus conséquente menée par les participants

PROGRAMME