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



Posted in #Formal Verification    #Certification    #SPARK   

About Yannick Moy

Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.