Remonter Suivant
Introduction

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.


Remonter Suivant