Le projet a pour objectif le développement de méthodes formelles
capables de vérifier, de manière fiable,
des propriétés multiformes, à la fois fonctionnelles
et non fonctionnelles (quantitatives)
apparaissant dans des problématiques industrielles.
Il s'appuiera sur les résultats acquis dans le projet RNRT Calife,
en consolidant certains d'entre eux (par exemple, mise en oeuvre de
résultats théoriques dans des outils de preuve)
ou en
généralisant notre cadre de travail
afin d'aborder des problèmes apparus en pratique.
Ainsi, certaines propriétés pertinentes
pour des protocoles comme PGM (Pragmatic General Multicast)
ou PIM (Protocol Independant Multicast)
dépassent le cadre du temps-réel
et s'expriment sous forme stochastique.
D'autres propriétés indispensables au bon fonctionnement
de logiciels embarqués ou mobiles portent
sur la consommation des ressources.
Le projet contribuera à conserver et renforcer la
position française dans ce domaine,
qui est actuellement reconnue
sur les outils de preuve, le model-checking
et ce au-delà du milieu académique
comme en témoigne l'émergence de compétences industrielles,
dans des sociétés comme Dassault Aviation, France Télécom
ou des PME comme Trusted Logic,
sans oublier
tout l'effort de développement qui s'est effectué autour de B.
Il faut cependant pour l'avenir immédiat tenir compte
du dynamisme américain,
particulièrement présent avec des outils comme PVS.
Comme dans Calife,
ce projet comporte des aspects fondamentaux,
des aspects applicatifs, et des aspects liés à l'interfaçage
des outils.
Les composantes fondamentales sont destinées
à élargir et durcir les technologies de spécification et de preuve.
Elles permettront la prise en compte
de propriétés non fonctionnelles,
et s'effectueront soit en modifiant le coeur des outils existants,
soit en construisant des bibliothèques performantes et spécialisées.
Les applications directement prise en compte dans le projet
relèvent des systèmes temps-réel embarqués.
Cependant il est clair que les retombées attendues
concernent plus largement les cibles privilégiées
des méthodes formelles.
C'est par exemple le cas dans le domaine de la sécurité
ou des cartes à puce,
où les utilisateurs de Coq
bénéficient déjà d'améliorations issues de Calife.
Les interfaces, enfin, permettront aux différents
outils de communiquer entre eux à partir d'un format commun,
issu d'une saisie graphique lorsque cela est possible.
Les outils logiciels résultant de ce projet seront
disponibles publiquement.