Preuve en Œuvre (Intégration de la preuve dans le développement logiciel) – ProofInUse

Inria est l'Établissement Public Scientifique et Technique français
dédié à l'informatique et l'automatique. L’équipe de recherche
Toccata est commune au centre Inria de Saclay et au Laboratoire de
Recherche en Informatique (UMR Université Paris-Sud et CNRS).
L'objectif de Toccata est de développer des méthodes et des outils
pour la vérification, avec un accent particulier sur la preuve
formelle. L'équipe développe et distribue des logiciels pour la preuve
de programme. Créée en 1996, la PME AdaCore est un éditeur français
indépendant de logiciel libre. Initialement centré sur le marché des
environnements de développement Ada, AdaCore a étendu son activité à la
fourniture d’outils de développement pour les applications critiques
embarquées. Elle a ainsi ajouté des outils de preuve formelle (SPARK,
en partenariat avec Altran) et d’analyse statique (CodePeer) aux
outils de développement Ada (GNAT Pro) qui constituent le cœur de son
offre. AdaCore sert une clientèle qui inclut la plupart des grands
noms de l’industrie aéronautique, spatiale, de la défense, du contrôle
aérien, du transport ferroviaire.

Plusieurs aspects du langage Ada étaient mal supportés par SPARK en
2014. La version SPARK 17.1 distribuée en 2017 intègre maintenant un
support solide entre autres pour les prédicats de type, les opérationsbit-à-bit, les calculs en virgule flottante et le code fantôme. Elle
exploite plus de prouveurs différents pour maximiser les taux de
réussite. Cette version intègre également un mécanisme de génération
de contre-exemples en cas d'échec de preuve, qui aide énormément les
développeurs à comprendre les raisons de ces échecs. Ces travaux
incorporent des nouveautés qui ont été reconnues dans le monde
académique par des publications en conférences internationales.

Les travaux se prolongent actuellement vers l'objectif à cours terme
de proposer un mécanisme interactif de traitement des conditions de
vérification non prouvées automatiquement. À plus long terme, nous
cherchons à promouvoir l'approche par preuve grâce à la fourniture de
composants logiciels déjà formellement spécifiés et prouvés. Nous
recherchons également à élargir l'offre en proposant des outils
similaires pour le langage C. Nous envisageons d'ouvrir le LabCom à
d'autres partenaires.

Coté académique, les travaux du LabCom ont donné lieu à 2 articles en
revues internationales et 8 communications dans des congrès
internationaux. L'environnement SPARK bénéficie d'un intérêt accru
aussi bien dans le monde académique que le monde industriel, en
particulier aux États-Unis, en Europe et au Japon. Au début du LabCom en 2014,
les clients de SPARK étaient principalement situés au Royaume-Uni.
En trois ans, le nombre de clients a doublé, avec une couverture mondiale :
Royaume-Uni toujours mais aussi France, Allemagne, Suède, Japon. En France
en particulier, de grands groupes industriels (Airbus et Thales) sont maintenant
clients de SPARK. Dans le même temps, l’intérêt académique pour la
technologie SPARK a décuplé, passant de quelques partenariats à plusieurs
dizaines de partenaires académiques. Aujourd’hui, AdaCore investigue
des opportunités d’utilisation de SPARK dans de nouveaux domaines tels
que l’automobile et les véhicules ou drones autonomes.

L'objectif du Laboratoire Commun ProofInUse est de proposer aux industriels des outils de vérification basés sur la preuve mathématique, qui visent à remplacer ou complémenter les activités de tests existantes, tout en réduisant les coûts de vérification. ProofInUse est issu du partage de ressources et de connaissances entre l'équipe de recherche Toccata, spécialisée en techniques de preuve de programmes, et AdaCore, PME éditrice de logiciels spécialisée dans la fourniture d'outils de développement pour les systèmes critiques. Une précédente expérience réussie de collaboration entre Toccata et AdaCore a permis de mettre la technologie Why3 développée par Toccata au cœur de la technologie
SPARK développée par AdaCore.

Le but du Laboratoire Commun ProofInUse est d'augmenter notablement le nombre d'industriels clients de la technologie SPARK, en démocratisant l'utilisation des techniques de preuve. Cette démocratisation passe par la résolution de plusieurs verrous scientifiques et techniques :

Un premier axe de recherche et d'innovation consistera à faciliter l'utilisation des prouveurs automatiques. Il s'agira d'abord de fournir une meilleure interaction avec l'utilisateur, en particulier pour débugger les spécifications non prouvables, comme ce qu'il est coutume d'attendre d'autres activités de développement. Ensuite, le Laboratoire Commun aura comme objectif d'améliorer le ratio de prouvabilité des programmes couramment utilisés dans l'industrie, en particulier pour le calcul numérique et les manipulation de données. En effet, l'intérêt économique des
techniques de preuve repose pour une grande part sur leur automatisation, dont toute amélioration se traduira par une attractivité accrue de la technologie SPARK. Ces deux points nécessiteront des avancées scientifiques en termes de support à la génération de contre-exemples et de modélisation des types de données adaptée aux capacités intrinsèques des prouveurs automatiques.

Un second axe de recherche et d'innovation consistera à permettre à l'utilisateur d'aller au-delà de ce qui est possible avec la technologie SPARK actuelle, en termes de spécification des programmes et de preuves de ces spécifications. Du côté spécification, il s'agira de supporter des constructions plus complexes dans la technologie Why3, qui permettent d'étendre le langage de programmation inclus dans SPARK. Cela permettra en particulier de satisfaire les utilisateurs qui veulent spécifier des propriétés d'invariance des données manipulées. Du côté preuves, l'ambition du Laboratoire Commun est de donner la possibilité à l'utilisateur de guider la preuve des propriétés les plus complexes, celles qui résistent aux prouveurs automatiques. Ces deux points nécessiteront des avancées scientifiques au niveau des constructions du langage intermédiaire utilisé pour la preuve, ainsi que des méthodes de génération d'obligations de preuve, afin de permettre ces utilisations.

L’équipe de recherche Toccata est commune au centre Inria de Saclay et au Laboratoire de Recherche en Informatique (UMR Université Paris-Sud et CNRS). Cette équipe développe et distribue des logiciels pour la preuve de programme. L'équipe Toccata collabore depuis près de dix ans avec des industriels utilisateurs de ces outils, dont Airbus, Dassault-Aviation, Gemalto.

AdaCore est une PME internationale, avec un effectif partagé pour moitié entre l'Europe et les États-Unis. AdaCore développe et distribue des logiciels pour le développement de systèmes critiques, en particulier l'environnement de développement GNAT Pro pour le langage de programmation Ada. AdaCore collabore depuis 2008 avec le groupe Altran autour de la technologie de preuve SPARK.