François PESSAUX
Contact
| Address: | ENSTA - 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.
Publications
