AdaCore Blog

Case Study for System to Software Integrity Includes SPARK 2014

by Yannick Moy

The NoseGear challenge was proposed at the Workshop on Theorem Proving in Certification as a small yet realistic case of critical system, to demonstrate and compare benefits and limitations of formal methods.

We have extended the scope of the challenge to add a logger and a GUI to the initial computation problem, to make it more realistic. We have developed an architecture of this system in AADL, a model of the computation in Simulink, code for the logger in SPARK and code for the GUI in Ada. Code is also automatically generated from AADL (to Ada) and Simulink (to SPARK), so that the complete concurrent application can be run with a simulator of the physical system. Verification activities include formal verification of the manual and generated SPARK code for absence of run-time errors and verification of properties expressed as contracts. All the artifacts (models, code, verification results) can be accessed from a prototype tool for agile certification, which records automatically traceability links between artifacts.

The paper we will present at ERTS explains the motivation behind this work, and the expected benefits when applied to actual systems

Attachments

Attachments

Posted in #Formal Verification    #Certification    #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, 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.