AdaCore Blog

New Guidance for Adoption of SPARK

by Yannick Moy

During 2016, AdaCore has collaborated with Thales to carry multiple experiments in applying SPARK to existing software projects in Ada. We discovered two things during these experiments:

  1. Adoption of formal verification, especially on existing projects, can be achieved in stages.
  2. Specific guidance is essential for adoption, both to define achievable objectives and to address the likely issues that will arise.

The stages we have defined are called Stone, Bronze, Silver, Gold and Platinum. They are described in the document called Implementation Guidance for the Adoption of SPARK that we co-authored with Thales. For each level, we define the benefits but also the impact on process and the costs and limitations. That's the high level view of each level. Then we give detailed guidelines on how to achieve that level on existing or new code.

What we discovered later was that the highest four levels (except Stone) map well with the verication objectives targeted at different DAL/SIL levels at Altran UK, with highest levels typically applied only at highest DAL/SIL levels (DAL A/SIL 4). The levels, guidelines and mapping with DAL/SIL were presented at the recent High Confidence Software and Systems conference.

Posted in #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK 2014, a product he presents in articles, conferences, classes and blogs (in particular www.spark-2014.org). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.