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