by Claude Marché and Johannes Kanig
Recent technological advances in formal deductive verification are benefiting industry users of programming language “Ada”. Mathematical proof complements existing test activities whilst reducing costs.
The Ada programming language was the winner of a call issued by the US Department of Defence in the late 1970’s, aiming at replacing the various languages that were used in mission-critical embedded software at that time. It was named in honour of Ada Lovelace, who is recognized by the scientific community as the first computer programmer. The first ANSI standard for Ada appeared in 1983.
SPARK, a subset of Ada, which has been around for nearly as long as Ada, was originally developed by Praxis (UK) and is currently co-developed by Altran UK and AdaCore (France and USA). Compared to Ada, SPARK imposes restrictions regarding the absence of name aliasing, allowing precise static analyses of data- and information-flow. These restrictions make SPARK well-suited to the development of mission-critical systems.
Unlike Ada, SPARK allows developers to attach contracts to procedures. A contract is a set of formal logic formulas expressing either requirements (pre-conditions) or guarantees (post-conditions) of the procedure to which it is attached. SPARK comes with a verification condition generator, allowing the user to statically check that contracts are fulfilled, using computer-assisted mathematical proof techniques.
SPARK has been used in several safety-critical systems, covering avionics (jet engines, air-traffic management), rail and space applications [1]. SPARK has also been used in the development of security-critical systems. Representative case studies include the NSA Tokeneer demonstrator (Microsoft Research Verified Software Milestone Award 2011) and the iFACTS system for assisting air-traffic controllers in the UK.
The AdaCore company leads the development of the GNAT Ada compiler and the many development tools around it. These tools are distributed under an open-source licence, which means no commitment for customers. Since AdaCore's business model is based on yearly subscriptions, the company must continually improve the technology and offer professional high-quality support. To maximize the potential dissemination of the innovative solutions, AdaCore also provides a free version of the tools suitable for development under the GNU public licence.
Ada2012, the current version of Ada language reference, now incorporates in its core the concept of contracts in the form of regular Ada Boolean expressions rather than formal logic formulas. The primary use of such contracts is for checking their validity during execution, so that their violation can be detected by testing instead of mathematical proof.
Figure 1: The SPARK2014 triptych.
SPARK2014 is the most recent generation of the SPARK tool suite (Figure 1). It is a full reimplementation of SPARK, developed jointly by Altran UK, AdaCore and the Toccata research team at the Inria-Saclay research centre in Orsay, France. Its main goal is to close the gap between testing and proving contracts: contracts can be checked for validity using computer-assisted proof, and testing can complement proofs when they fail [2] (Figure 2). An additional novelty is the incorporation of state-of-the-art technologies for automated theorem proving, thanks to the use of Toccata's Why3 environment and its ability to call the best SMT solvers in the market. This technology has enabled fully automatic discharge of a far greater percentage of verification conditions.
Figure 2: Snapshot of the GPS user interface for Ada and SPARK, displaying a program under development. The red line corresponds to a warning issued by the proof tool.
SPARK2014 will continue to evolve in the near future. A new 3-year project "ProofInUse", funded by the French National Research Agency, started in April 2014. Its aim is to promote the replacement of testing activities by proof methods to the Ada industry community. To this end, a significant effort will be made to even further automate the approach. We also plan to enlarge the subset of Ada covered by the SPARK language, enabling more applications to be developed using SPARK2014’s powerful hybrid approach of test and proof. Among the new features, the SPARK verification condition generator will fully support the IEEE-754 standard for floating-point arithmetic, thanks to the expertise of the Toccata team in this domain [3]. Thus, applications making important use of numerical computations, such as in avionics and space control software, will be able to reach a very high level of assurance in the precision of computations.
Links:
http://libre.adacore.com/
http://www.spark-2014.org/
References:
[1] R. Chapman, F. Schanda: “Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK”, 5th Int. Conf. on Interactive Theorem Proving, 2014.
[2] C. Dross et al.: “Rail, Space, Security: Three Case Studies for SPARK2014”, 7th European Congress on Embedded Real Time Software and Systems, 2014.
[3] S. Boldo, C. Marché: “Formal verification of numerical programs: from C annotated programs to mechanical proofs”, Mathematics in Computer Science, 2011.
Please contact:
Claude Marché, Inria, France
Tel: +33 172 925 969
E-mail:
