Tool Seminar:SPARK Lecture
From Dependability
| Overview | | Schedule | | Syllabus | | 2006 Project Guidelines | | Tool List | | Editing Guidelines |
SPARK Ada is an annotated subset of Ada developed by Praxis High-Integrity Systems for use in safety-critical applications. The language restricts Ada to a linear type system (no aliasing of any kind) and to control-flow constructs that are amenable to powerful static analysis. The result is a very small language in which it is much easier to reason about program behavior than is typical of programs written in languages such as C, C++ or Java.
SPARK Ada adds to the subset of Ada it defines a set of powerful annotations used to describe program properties. The static analysis tools that come with the SPARK toolset, the SPARK Examiner and SPARK Simplifier, read the annotation and the code and attempt to automatically prove that the code complies with the properties specified in the annotations. Properties that cannot be automatically proved are presented to the user as proof obligations, and can be discharged either by manual inspection or through the provided human-guided theorem prover.
Experience from various industry projects suggest that as many as 90% fewer bugs are introduced into a system built in Ada, rather than C. Further evidence suggests that as many as 90% fewer bugs are introduced into a system built in SPARK Ada rather than unconstrained Ada. That makes nearly 99% fewer bugs if a system is built in SPARK Ada rather than C.
So why don't we all use SPARK Ada?
In this presentation, Tony will introduce the language and work through several examples, showing program text, tool output, and proof execution. By the end of the lecture, you should have at least a fuzzy feeling for what SPARK does, can do, and doesn't do well at all.
As a starting point, please download and read a recent journal paper written by Peter Amey, the "father" of SPARK:
For safety and mission critical systems, verification and validation activities frequently dominate development costs, accounting for as much as 80 percent in some cases. There is now compelling evidence that development methods that focus on bug prevention rather than bug detection can both raise quality and save time and money. A recent, large avionics project reported a four-fold productivity and 10-fold quality improvement by adopting such methods. A key ingredient of correctness by construction is the use of unambiguous programming languages that allow rigorous analysis very early in the development process.
We will not discuss the paper during the lecture, but it provides good foundation. It is also quite short.
 link
| Correctness by Construction: Better can also be Cheaper |