SPARK 2014: Formal Program Verification For All
Presented as part of the 2014 HCSS conference.
Abstract:
SPARK is a programming language targeted at safety- and security-critical applications. SPARK builds on the strengths of the Ada programming language for creating highly reliable and long-lived soft- ware. SPARK restrictions ensure that the behavior of a SPARK program is unambiguously defined, and simple enough that formal verification tools can perform an automatic diagnosis of conformance between a program specification and its implementation. The SPARK language and toolset for formal verification have been applied over many years to on-board aircraft systems, control systems, cryptographic systems, and rail systems [4].
The latest version, SPARK 2014, builds on the new specification features added in Ada 2012 [1], so formal specifications are now expressed in the same language as programs, which also means that they are understood by the usual development tools and can be executed. Care was taken to match the formal proof semantics with the run-time assertion checking semantics (including possible run-time errors in formal specifications, and floating-point semantics). As a result, formal specifications can be tested and debugged like code, which goes a long way to making them accessible to all programmers.
Two other features of the new toolset contribute to this democratization of formal verification. The level of proof automation obtained by using state-of-the-art generators and provers of Verification Condi- tions makes fully automated proof within reach. User interaction is made practical and efficient through IDE integration, mechanisms for proof reuse, possible analysis of single components, and detailed feed- back on failed proofs.
Yet, the most important enabler for industrial adoption is the integration in existing processes, for existing codebases. Formal verification can be combined with test of the executable produced with a special instrumentation of the compiler [2]. Going further in the direction of combining formal verification and other methods, we have proposed a framework for managing the assumptions upon which proof relies [3]. The toolset gives complete control to users over which components or subcomponents of a program are formally verified, which allows gradual adoption in brown fields.
The largest application of SPARK 2014 so far is a case study by the Space Systems division of Airbus Defence & Space, developed during three years along with the new language and tools. The success of this case study has prompted the decision to start a new one-year pilot project targeting the potential use of SPARK 2014 in the future Ariane 6. During the talk, I will use the Airbus Defense & Space case study to present the key features of the language and the tools, including a presentation of the actual user interaction inside an IDE, and I will finish with a focus on the combination of test and proof in relation to DO-178C.
---
[1] J. Barnes. Ada 2012 Rationale. 2012
[2] C. Comar, J. Kanig, and Y. Moy. Integrating formal program verification with testing. In International Conference on Embedded Real Time Software and Systems, 2012.
3] J. Kanig, R. Chapman, C. Comar, J. Guitton, Y. Moy, and E. Rees. Explicit assumptions - a prenup for marrying static and dynamic program verification. In Submitted to the International Conference on Test & Proof, 2014.
[4] I. O’Neill. SPARK – a language and tool-set for high-integrity software development. In Industrial Use of Formal Methods: Formal Verification. Wiley, 2012.
Presenter Bio:
Yannick Moy is a Senior Software Engineer at AdaCore, where he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties.
Yannick lead the three-years project Hi-Lite leading to the new version of SPARK known as SPARK 2014. He presented SPARK at many international conferences and events, and is used to teaching SPARK trough classes, webinars and blogs. Yannick previously worked on source analyzers for PolySpace (now The MathWorks) and INRIA Research Labs.