Sites Inria

English version

LabCom

A.B. (*) -

LabCom ProofInUse : AdaCore & l'équipe-projet Toccata

En 2014, Inria et la société AdaCore ont lancé un laboratoire commun baptisé ProofInUse pour une durée de trois ans. Ce laboratoire commun avait pour objet 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 avait permis de mettre la technologie Why3 développée par Toccata au cœur de la technologie SPARK développée par AdaCore .

  • L’entreprise

Créée en 1996, AdaCore est une société éditrice française indépendante de logiciel libre. Initialement centrée 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 Inria), d’analyse statique (CodePeer ) et de développement basé sur les modèles (QGen ) 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 et du transport ferroviaire. Avec sa filiale américaine Ada Core Technologies Inc. , elle réalise un chiffre d’affaires global d’environ 20 millions d’euros pour une centaine d'employés.

  • L’équipe Inria

L’équipe-projet Inria Toccata est une équipe commune d’Inria-Saclay et du Laboratoire de recherche en informatique (UMR Université Paris-Sud et CNRS), dont l'objectif est de développer des méthodes et des outils pour la vérification, avec un accent particulier sur la preuve formelle. Les activités de recherche de Toccata se déclinent en quatre axes : vérification déductive de programmes, démonstration automatique, vérification de programmes numériques, et certification des outils. Le LabCom ProofInUse concerne principalement le premier de ces axes, en particulier les travaux autour du développement du logiciel Why3 .

  • Objet du Laboratoire

L'objectif du LabCom ProofInUse était de proposer aux industriels des outils de vérification basés sur la preuve mathématique, pour remplacer ou complémenter les activités de tests existantes, tout en réduisant les coûts de vérification. Le but était d'augmenter notablement le nombre d'industriels clients de la technologie SPARK , en démocratisant l'utilisation des techniques de preuve.

  • Résultats

Les contributions ont été aussi bien effectives sur le plan académique que sur les résultats de transfert industriel. Côté académique, les travaux du LabCom ont donné lieu à trois publications en revues internationales et dix publications en conférences internationales avec comité de lecture.

Côté transfert, les succès d'adoption de SPARK pendant la durée du LabCom ont été réalisés dans les domaines spatial et de la défense. Une collaboration avec Thales a donné lieu à l'écriture conjointe d'un guide public d'adoption de SPARK entre AdaCore et Thales , utilisé à la fois par d'autres équipes chez Thales et par des équipes d'autres sociétés. Ces succès initiaux devraient être suivis d'autres dans le domaine avionique et les domaines connexes : trafic aérien, ferroviaire et sécurité (avec pour chacun déjà des clients SPARK importants) ; spatial et défense. SPARK commence également à être utilisé dans les domaines des appareils médicaux et des véhicules autonomes (voitures, drones).

Enfin, deux des trois ingénieurs Inria embauchés pendant la durée du LabCom ont été recrutés par AdaCore .   

  • Suites actuelles

Le laboratoire commun Inria continue et une nouvelle étape est actuellement en cours, portée par l’équipe Toccata, avec AdaCore comme partenaire mais également avec l’extension à un partenaire additionnel. Le logiciel Why3 continue à être utilisé par des acteurs industriels ou académiques, ainsi que dans l’enseignement.


Lorsque nous avons cherché en 2010 à moderniser notre outil d'analyse formelle de programmes, nous nous sommes naturellement tournés vers l'équipe Toccata qui développait déjà l'outil Why3 et qui avait montré son avance scientifique et sa maturité technologique lors d'expériences d'adoption industrielle réussies. Nous avons embauché deux anciens doctorants de cette équipe et monté un projet collaboratif avec Toccata, puis un LabCom, et nous poursuivons cette collaboration aujourd'hui à travers le projet d’un nouveau laboratoire commun Inria. Le choix fait par l'équipe Toccata de développer des logiciels sous licence libre et leur soutien continu aux utilisateurs industriels ont été déterminants dans le succès de cette aventure commune

                                                                                   Cyrille Comar, Président d'AdaCore


Pour l’équipe de recherche Toccata, la collaboration avec la PME AdaCore au travers du laboratoire commun ProofInUse est très fructueuse. La présence de deux ingénieurs Inria à temps plein sur le projet, qui passent la moitié de leur temps sur le site de l’entreprise, autorise une collaboration très rapprochée qui nous permet d’être au plus près des défis posés par les applications industrielles. La cerise sur le gâteau est que ces travaux donnent également lieu à des publications académiques de haut niveau.

                   Claude Marché, responsable de l’équipe Toccata et porteur du laboratoire ProofInUse

 

Mots-clés : Systèmes critiques Adacore Toccata Développement de logiciels LabCom

Haut de page

Suivez Inria