François PESSAUX
Contact
| Address: | ENSTA paris - U2IS 828, Boulevard des Maréchaux 91762 Palaiseau Cedex France |  |
| Office: | R223 | |
| Email: | ||
| Tel.: | +33 1 8187 2073 |
Ma page personnelle : François Pessaux
Activité de recherche
Mes travaux visent principalement à fournir des outils de développement pour la réalisation de logiciels requérant un haut niveau de sûreté en utilisant les méthodes dites formelles. Ce travail s'inscrit dans la continuité de mes travaux du LIP6 sur l'environnement FoCaLize et consiste à continuer à concevoir, développer et maintenir cet environnement. La page principale de FoCaLiZe peut être consultée ici, permettant l'accès aux dernières nouvelles, aux téléchargements, à la documentation, aux ressources et au bug tracker. L'idée est de faire disparaître la multiplicité d'outils différents entre la spécification du logiciel, son implémentation et les preuves des exigences de sûreté. Le fait de pouvoir énoncer des propriétés (spécifications), des algorithmes (implantation) et des preuves que ces derniers satisfont effectivement les spécifications, le tout dans un même langage permet d'accroître la confiance que l'on peut avoir en un développement. Ces 3 éléments doivent ensuite être transformés en d'une part un modèle exécutable et d'autre part un modèle formel, ce dernier devant être vérifié par un outil de preuve. Une contrainte importante est que le langage de développement doit rester relativement simple et proche de ce dont on a l'habitude dans le monde du développement, la complexité du plongement dans un système formel devant être le plus possible à la charge du compilateur de ce langage. Le compilateur FoCaLiZe prend donc en entrée un "programme" dans lequel sont énoncés des propriétés, des algorithmes et des preuves que ces propriétés sont vérifiées, bien souvent au travers des algorithmes énoncés. Il génère deux sorties. D'une part un programme en OCaml destiné à devenir exécutable (si le "programme" FoCaLiZe n'est pas uniquement un modèle de spécification). D'autre part un modèle formel complet (propriétés, algorithmes et preuves) en Coq. Ce dernier, un assistant de preuve, aura à charge de vérifier la cohérence de ce modèle afin d'en certifier la correction formelle. Ainsi, l'assistant de preuve ne fait pas les preuves: il les vérifie seulement. La rédaction des preuves reste à la charge de l'utilisateur, en langage FoCaLiZe, mais est aidé par des prouveurs automatiques couplés à FoCaLiZe. Actuellement, un seul est utilisé: zenon, développé par Damien Doligez de l'INRIA, mais l'architecture du langage et du compilateur FoCaLiZe est conçue pour n'importe quel autre prouveur dédié à telle ou telle forme de propriétés. Comme précisé précédemment, les constructions que FoCaLiZe offre peuvent être utilisées à des fins de modélisation sans "programmation", ce qui permet de l'intégrer dans un cycle de conception plus orienté "système" que "logiciel" ("orienté spécifications"). Dans l'état actuel des travaux sur FoCaLiZe, les propriétés sont énoncées en logique du premier ordre au travers de la syntaxe du langage. Rien n'interdit a priori d'envisager l'interface avec d'autres formalismes de description (UML, SysML, etc.) tant que les propriétés que ces derniers permettent d'énoncer restent dans ce formalisme logique. L'étude de l'extension de FoCaLiZe à d'autres formes de propriétés (temporelles, synchrones), donc d'autres formalismes logiques est un problème actuellement ouvert et constitue un des axes de recherche pour le futur. En effet, dans le cadre de systèmes embarqués, il serait intéressant de pouvoir exprimer et prouver des propriétés d'état (techniquement, des valeurs mutables), des propriétés de synchronisation (aspects à la Lustre, Lucid Synchrone...). Outre des problèmes d'extension des constructions du langage, des problèmes de choix de logique, donc de vérificateur formel du modèle généré, peuvent se poser, voire même des problèmes de modèle selon lequel FoCaLiZe représente formellement le système. En effet, adresser une plus large classe de propriétés à exprimer et à prouver (en vue d'augmenter l'expressivité de modélisation) peut ne pas être sans impact sur la manière de modéliser ce système en vue de son implantation et de sa vérification.Activité d'enseignement
- 2012-2013, Algorithmique et programmation (IN101, ENSTA 1A)
- 2011-2013, Principes des langages de programmation (INE11, ENSTA 2A). Avec Michel Mauny.