AdaCore Blog

Use of SPARK in a Certification Context

by Yannick Moy

One possible reason to choose SPARK over other solutions is the benefits that it brings in a certification context, for reaching some of the verification objectives. For example, the previous version of SPARK has been used both in a safety certification context and in a security certification context. With SPARK 2014, we target in particular the avionics domain, whose recently updated certification standard DO-178C accepts the use of formal verification as justification for many verification objectives.

While certification authorities in railway have long recognized the use of formal methods, and a few companies like Airbus and Rockwell Collins have pioneered the use of formal methods in avionics, we still are at the beginning of the adoption of formal methods in industries submitted to certification constraints. Which means that many people simply don't know yet how they should present the use of formal methods to the certification authorities to obtain the credit they expect from it.

This was the reason that pushed in 2010 for the creation of the workshop on Theorem Proving in Certification. Since then, the group has had 3 gatherings in Oxford, the last of which in December last year, during which we decided to work on a shared document gathering recommandations for the use of formal methods in certification. This draft document is now publicly available here:

https://docs.google.com/document/d/1nTXzxHLXg9s97mxtrEOS8rfgUNGK3dnW7L43WwU7Lpo

If you're interested in this topic, don't hesitate to send comments about the above document to the public mailing-list tpcert@googlegroups.com. You can also participate more actively in the discussions by joining the googlegroup.

Posted in #Formal Verification    #Certification   

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, a product he presents in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.