Proof in Use (Integration of Proof in Software Development) – ProofInUse
Verification of Safety and Security Critical Software by Formal Proof
Integrate methods and tools, at the cutting edge of academic research in formal methods, within an industrial environment for critical software development.
Proposing verification tools based on mathematical proof, aimed at complementing testing activities while reducing costs.
The ProofInUse joint lab targets software manufacturers developing systems that are critical<br />for safety and security. The objective is to propose new verification tools based on<br />mathematical proof. AdaCore's SPARK environment specializes in software development in<br />Ada for critical systems. The solution proposed by ProofInUse is the integration into SPARK<br />of the Why3 verification environment, developed by the Toccata research team. This<br />integration work aims at making the proof tools, at the state-of-the-art of academic research,<br />more accessible to developers of critical software. Integration is designed to allow for a<br />progressive transition from testing and review of code to proof. The use of formal proof by<br />non-specialists is facilitated by an increase in the success rate of automatic provers and, in the<br />case of proof failures, by a better feedback to the user. The main expected impact is the<br />significant increase in the number of industrial customers using SPARK technology.
Inria is the French, scientific and technical, public institution dedicated to computer science
and control. The Toccata research team is common to the Inria center in Saclay and to the
Laboratoire de Recherche en Informatique (UMR Université Paris-Sud and CNRS).
Toccata's objective is to develop methods and tools for verification, with particular emphasis
on formal proof. The team develops and distributes software for deductive program
verification. Created in 1996, the AdaCore SME is an independent French publisher of free
software. Initially focused on the Ada development environment market, AdaCore has
expanded its business to provide development tools for embedded critical applications. It has
added formal proof tools (SPARK, in partnership with Altran) and static analysis (CodePeer)
to Ada development tools (GNAT Pro), which form the core of its offering. AdaCore
customers include many of the leading companies in the aeronautics, space, defense, air
traffic control and railway industries.
Several aspects of the language were poorly supported by SPARK in 2014. The SPARK
version 17.1 released in 2017 now includes robust support for type predicates, bit-wise
operations, floating-point computations and ghost code. It exploits several more back-end
provers to maximize success rates. This version also includes a counterexample generation
mechanism in case of proof failure, which greatly helps developers understand the reasons
for these failures. This work incorporates innovations that have been recognized by the
academic world through publications in international conferences.
Work is now extending towards the short-term objective of providing an interactive
mechanism for discharging unproved verification conditions. In the longer term, we seek to
promote the proof-based approach by providing software components that are already
formally specified and proven. We are also looking to expand the offering by proposing
similar tools for the C language. We plan to open the LabCom to other partners.
On the academic side, the work of the LabCom resulted in 2 articles in international journals
and 8 papers in international congresses. The SPARK environment benefits from increased
interest in the academic world as well as in the industrial world, particularly in the United
States, Europe and Japan. At the beginning of the LabCom in 2014, SPARK customers were
mainly located in the UK. In three years, the number of customers has doubled, with
worldwide coverage: United Kingdom still but also France, Germany, Sweden, Japan. In
France in particular, large industrial groups (Airbus and Thales) are now customers of
SPARK. At the same time, the academic interest in SPARK technology has increased tenfold,
from a few partnerships to dozens of academic partners. Today, AdaCore is investigating
opportunities to use SPARK in new areas such as automotive, autonomous vehicles or
unmanned aircrafts.
The objective of the Joint Laboratory ProofInUse is to provide verification tools, based on mathematical proof, to industry users. These tools would be aimed at replacing or complementing the existing test activities, whilst reducing costs. ProofInUse originates from the sharing of resources and knowledge between the Toccata research team, specializing in techniques for program proofs and the SME AdaCore, a software publisher, specializing in providing software development tools for critical systems. A previous successful collaboration between Toccata and AdaCore enabled Toccata’s Why3 technology, to be put into the heart of the AdaCore-developed SPARK technology.
The purpose of the Joint Laboratory ProofInUse is to increase significantly the number of industrial customers of the SPARK technology, thus democratizing the use of proof techniques. This democratization requires the resolution of several scientific and technological challenges:
A first axis of research and innovation is to facilitate the use of automatic provers. This first aspect requires the provision of a better interaction with the user, especially for debugging non-provable specifications as it is customary to expect for other development activities. Then, the Joint
Laboratory will aim at improving the ratio of provability of programs commonly used in industry, in particular for numerical computations and data manipulations. Indeed, the economic interest of proof techniques is based largely on their automation, hence any improvement in this respect will result in the SPARK technology becoming more attractive. These two points require scientific breakthroughs in terms of support to the generation of counter-examples and modeling of data types adapted to the intrinsic capacities of automated provers.
A second axis of research and innovation is to allow the user to go beyond what is possible with the current SPARK technology, in terms of specification of programs and the proofs of these specifications. On the specification side, it will require the support for more complex constructions in the Why3 technology, permitting the extension of the programming language included in SPARK. This will, in particular, satisfy the user’s need to specify data invariants. On the proof side, the objective of the Joint Laboratory is to give the user the possibility to guide the proof for more complex properties - for instance, those resistant to automated provers. These two points require scientific advances not only at the level of the intermediate language constructs used for proofs, but also in the methods for generating proof obligations, permitting these uses.
The Toccata research team is part of INRIA Saclay and the Laboratoire de Recherche en Informatique (UMR Université Paris-Sud and CNRS). This team develops and distributes software for program proof. The Toccata team collaborated for nearly ten years with industry users of these tools, including Airbus, Dassault-Aviation, Gemalto.
AdaCore is an international SME, with a workforce shared between Europe and the United States. AdaCore develops and distributes software for the development of critical systems, in particular the GNAT Pro development environment for the Ada programming language. AdaCore has worked since 2008 with the Altran group around the SPARK proof technology.
Project coordination
Claude Marché (Institut National de Recherche en Informatique et en Automatique)
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
Partner
Inria Saclay - Île-de-France Institut National de Recherche en Informatique et en Automatique
Help of the ANR 300,000 euros
Beginning and duration of the scientific project:
- 36 Months
