ProofInUse is a new public-private laboratory, co-managed by Inria and AdaCore. It is a a major new partnership to increase the use of evidence-based verification tools in the software industry: sour objective is to provide software audit tools based on mathematical proof to industrial players, thus aiming to replace or complement existing testing activities, while reducing verification costs for the aerospace, transport, medical and aeronautics industries ...
The ProofInUse joint laboratory led by Inria, the French National Institute for Research in Computer Science and Control, and AdaCore, the leading provider of software solutions for the Ada language, aims to spread the use of formal proof tools. These tools complement or replace existing software development activities while reducing verification costs.
Partly funded by the French government, the joint laboratory was launched with a one-day conference on Monday 2 February in Paris. Speakers came from Inria, AdaCore, Oxford University, OCamlPro and the CEA (French Atomic Energy Commission). In addition to AdaCore and Inria, the sponsors of the joint laboratory include Altran, ANR (Agence Nationale de la Recherche), CNRS (Centre National de la Recherche Scientifique) and Université Paris-Sud. The theme of the ProofinUse labcom is in line with one of the scientific priorities of the Inria Saclay - Ile-de-France centre relating to safety, security and reliability for architectures, software and data.
Objective: democratize the use of evidence techniques
"Software verified with these formal techniques will be more reliable and less expensive to develop, promise the people in charge of the lab.
The place of software in critical systems has been growing steadily since the year 2000, through a multitude of uses (transport, medicine...). In many areas, software flaws can have serious consequences, human or financial. To establish the robustness of these applications, formal methods, such as the use of formal proof, offer financial and security advantages. The use of mathematical proof simplifies the verification process and minimizes its cost. A joint AdaCore / Toccata laboratory, ProofInUse, was created in April 2014. ProofInUse aims to offer industrial companies tools to verify their software and thus democratize the use of proof techniques.
Why not enjoy unlimited reading of UP'? Subscribe from €1.90 per week.
The deployment of these techniques allows for increased automation of audit activities, which reduces the cost and time to develop critical software. ProofInUse is based on SPARK technology for the development of critical applications, a technology developed by AdaCore and Altran.
ProofInUse will therefore provide a laboratory for research on evidence techniques, the objective being that this research will make it possible to respond to the technological and scientific challenges that arise. The research will include facilitating the use of automatic demonstrators and extending SPARK's capabilities to verify more complex properties.
"Verification tools based on mathematical proof have previously been developed in the academic world, and have proven to be effective in finding bugs in complex critical software, "says Claude Marché, Inria research director. "Thanks to our collaboration with AdaCore, ProofInUse will allow us to continue to develop these techniques by integrating them further into traditional software development processes, to ensure that they can be successfully applied in an industrial context.
ProofInUse was born from the sharing of resources and knowledge between AdaCore and the Toccata research team, which specializes in program proofing techniques. In a previous collaboration between AdaCore and Toccata, Toccata's Why3 technology was integrated into the core of AdaCore's SPARK technology.
"We live in a world where software is becoming more and more important, where it's becoming more and more important that programs are reliable, safe and secure," says Cyrille Comar, President of AdaCore.
"Developing formal evidence-based techniques within SPARK by ensuring that they are fully integrated with other verification techniques such as testing is a big step towards reducing the cost and time of verification activities without losing security. The public/private collaboration within ProofInUse will give a new impetus to disseminate evidence-based verification techniques more widely and increase the industrial use of these techniques, which should benefit both industry and the general public. »
Target market: software development assistance
The market targeted by the Joint ProofInUse Laboratory is that of development aid:
- certified critical applications (examples: DO-178, EN 50126, ECSS-E-40B, ISO 26262, etc.) at the most demanding levels
- security applications certified to level 5 or higher of the Common Criteria.
This concerns both domains where the Ada language is already widely used (avionics, space, railways) and domains using other languages (C, C++, Java, mainly) in which the new possibilities of proof and test integration provided by the SPARK technology will allow a progressive conversion.
The advances obtained through the work carried out in the ProofInUse Joint Laboratory will be integrated into successive versions of the software developed by Toccata and AdaCore.
