ProofInUse est un nouveau laboratoire public-privé, cogéré par l’Inria et AdaCore. Il s’agit là d’un nouveau partenariat majeur dans le but d’augmenter l‘utilisation des outils de vérification basés sur les preuves mathématiques au sein de l’industrie du logiciel : son objectif est de fournir des outils de vérification de logiciels basés sur la preuve mathématique à des acteurs industriels, visant ainsi à remplacer ou à complémenter les activités existantes de tests, tout en réduisant les coûts de vérification pour l’aérospatial, le transport, la médecine ou encore l’aéronautique …
Le laboratoire commun ProofInUse conduit par Inria, l’Institut National de Recherche en Informatique et Automatique, et AdaCore, le principal fournisseur de solutions logicielles pour le langage Ada, a pour but de répandre l’utilisation d’outils de preuves formelles. Ces outils complètent ou remplacent les activités existantes du développement logiciel tout en réduisant les coûts de vérification.
En partie financé par le gouvernement français, le laboratoire commun a été lancé par une journée de conférence ce lundi 2 février à Paris. Les intervenants viennent d’Inria, AdaCore, l’université d’Oxford, l’entreprise OCamlPro et le CEA (Commissariat à l’Énergie Atomique). Outre AdaCore et Inria, les sponsors du laboratoire commun comptent Altran, l’ANR (Agence Nationale de la Recherche), le CNRS (Centre National de la Recherche Scientifique) et l’Université Paris-Sud. Le thème du labcom ProofinUse s’inscrit dans l’une des priorités scientifiques du centre Inria Saclay – Ile-de-France relative à la sûreté, sécurité et fiabilité pour les architectures, les logiciels et les données.
Objectif : démocratiser l’utilisation des techniques de preuve
« Les logiciels vérifiés avec ces techniques formelles seront plus fiables et moins coûteux à développer », promettent les responsables du laboratoire.
La place des logiciels dans les systèmes critiques n’a cessé de croître depuis l’an 2000, à travers une multitude d’utilisations (transports, médecine…). Dans de nombreux domaines, les failles de logiciel peuvent avoir de graves conséquences, humaines ou financières. Pour asseoir la robustesse de ces applications, les méthodes formelles, telle que l’utilisation de la preuve formelle, offrent des avantages financiers et de sécurité. L’utilisation de la preuve mathématique simplifie le processus de vérification et en minore le coût. Un Laboratoire commun AdaCore / Toccata, ProofInUse, a été créé en avril 2014. ProofInUse souhaite proposer aux industriels des outils de vérification de leurs logiciels et ainsi démocratiser l’utilisation des techniques de preuve.
Pourquoi ne pas profiter d’une lecture illimitée de UP’ ? Abonnez-vous à partir de 1.90 € par semaine.
Le déploiement de ces techniques permet d’accroître l’automatisation des activités de vérification, ce qui réduit les coûts et le temps de développement des logiciels critiques. ProofInUse se base sur la technologie SPARK pour le développement d’applications critiques, une technologie développée par AdaCore et Altran.
ProofInUse va donc fournir là un laboratoire pour la recherche sur les techniques de preuves, l’objectif étant que ces recherches permettent de répondre aux défis technologiques et scientifiques qui se posent. Les recherches vont notamment viser à faciliter l’utilisation de démonstrateurs automatiques et à étendre les capacités de SPARK pour vérifier des propriétés plus complexes.
« Les outils de vérification basés sur la preuve mathématique ont précédemment été développés au sein du monde académique, ils ont fait leurs preuves pour trouver des bugs dans des logiciels critiques complexes, » déclare Claude Marché, directeur de recherche Inria. « Grâce à notre collaboration avec AdaCore, ProofInUse permettra de continuer à développer ces techniques en les intégrant davantage dans les processus traditionnels de développement logiciel, pour s’assurer qu’elles peuvent être appliquées avec succès dans un contexte industriel ».
ProofInUse est né du partage des ressources et des connaissances entre AdaCore et l’équipe de recherche Toccata, spécialisée dans les techniques de preuves de programmes. Lors d’une précédente collaboration entre AdaCore et Toccata, la technologie Why3 de Toccata a été intégrée au cœur de la technologie SPARK d’AdaCore.
« Nous vivons dans un monde dans lequel les logiciels prennent chaque jour une place plus importante, où il devient toujours plus important que les programmes soient fiables, sûrs et sécurisés, » déclare Cyrille Comar, président d’AdaCore.
« Développer les techniques basées sur la preuve formelle au sein de SPARK en veillant à les intégrer complètement avec d’autres techniques de vérification telles que les tests est un grand pas pour réduire les coûts et la durée des activités de vérification sans perdre en sûreté. La collaboration public/privé au sein de ProofInUse va donner un nouvel élan pour diffuser plus largement les techniques de vérification basées sur la preuve et accroître l’utilisation industrielle de ces techniques, ce qui devrait bénéficier autant aux industriels qu’au grand public. »
Marché visé : l’aide au développement logiciel
Le marché visé par le Laboratoire Commun ProofInUse est celui de l’aide au développement :
– d’applications critiques certifiées (exemples : DO-178, EN 50126, ECSS-E-40B, ISO 26262, etc.) aux niveaux les plus exigeants
– d’applications de sécurité certifiées selon le niveau 5 ou supérieur des critères communs.
Cela concerne à la fois les domaines où le langage Ada est déjà largement présent (avionique, spatial, ferroviaire) et les domaines qui utilisent d’autres langages (C, C++, Java, principalement) dans lesquels les possibilités nouvelles d’intégration de la preuve et des tests que fournira la technologie SPARK permettront une conversion progressive.
Les avancées obtenues par le travail effectué dans le Laboratoire Commun ProofInUse seront intégrées aux versions successives des logiciels développés par Toccata et par AdaCore.
