Ada Watch: Choosing the right Ada subset for strong static guarantees
BlogAugust 13, 2013
Yannick Moy
AdaCore
While Ada offers many features that act as safety guards at run time, by raising exceptions when a violation is detected, some of these features may be too complex to guarantee a safe execution before the program is run. This is the case for example of pointers, which may be used to create arbitrarily complex shared data structures in memory. SPARK is a subset of Ada that forbids these features, most notably pointers, in order to be able to provide strong guarantees at compile time. A preview of the next revision of SPARK called SPARK 2014 is already available, as well as the associated verification tools.
Although SPARK evolution has followed the evolutions of Ada, with a new version of SPARK for each new version of Ada (SPARK 83, SPARK 95, SPARK 2005), the new revision SPARK 2014 is quite different in a number of aspects. SPARK 2014 is the result of a project started in 2010 with the objective of making it cost-effective to use formal verification instead of testing for critical software. Just a few months before, Airbus had presented their five “must-have” criteria for adopting a formal method: soundness, applicability to the code, usability by “normal” engineers on “normal” computers, improve on classical methods, certifiability. We have had these five criteria very much in mind during these three years, and here are the results for SPARK 2014 and the associated verification tool GNATprove.
Soundness:
This is the cornerstone of the language and the tools. It is not limited to saying: "we use Hoare logic". What we want to achieve is "maximum" soundness: not only the tools cannot state wrong properties when you use them appropriately, but it should not be easy to get a false sense of confidence in the software by misusing the tools (for example by stating a wrong axiom). Many decisions were taken to ensure maximum soundness, like forbidding users from stating axioms.
Applicability to the code:
SPARK 2014 is the largest possible subset of Ada that still makes it possible to do formal verification. In particular, it includes generics, tagged types, discriminants, dynamic types, early returns, and many other features that were excluded from SPARK 2005. And we have made it possible to combine formal verification with testing, for those parts of the code that cannot be formally analyzed. So it's not an all-or-nothing technology, but one that you can introduce in any Ada project really.
Usability by normal engineers:
This is the issue that made us most busy all these years. First, we have achieved a level of automation where most proofs go through automatically, in particular the proofs of absence of run-time error. Secondly, we have tightly integrated the tools in the developer workflow (for example, through use of project files and automatically computed dependencies) and development environment (for example, the ability to run GNATprove on a specific subprogram or line of code, and the display of problematic program paths).
Improve on testing:
The fact that formal verification is exhaustive makes it an ideal replacement for the costly unit-testing activity mandated for critical software. The main challenge here was to facilitate progressive adoption of formal verification. Because the subprogram contracts needed for formal verification are already useful for testing, and because GNATprove can be applied separately to individual SPARK subprograms in any Ada program, switching to formal verification can be done in a matter of days.
Certifiability:
When we started the project, the formal methods supplement for the avionics standard DO-178 was not yet finalized. Since then, it has been published with the new version of the standard, DO-178C, so today, GNATprove can be used instead of testing for critical embedded programs in planes developed at the highest levels A or B. We have published a paper in IEEE Software on how to deal with the subtle issue of coverage in that case. Of course, projects in other domains in which formal methods are already recognized (for example, railway) may also use GNATprove.
The results of the industrial case studies developed in the project are publicly available, for others to get a feeling at what the new technology is good at, and the current stage of development. Perhaps the most frequent comment, when users switched from previous SPARK technology to this new SPARK 2014 one, was the incredible usability improvement provided by the ability to execute specifications. This kind of combination of dynamic techniques and static ones is certainly promising for the future of software verification.
