Articles 1 - 2
Avionics
Formal program verification in avionics certification - Story
February 24, 2017
Five years after the official adoption of the new DO-178C/ED-12C standard and its supplements, including the DO-333/ED-216 supplement on formal methods, no avionics-certification project has yet acknowledged using this new supplement. However, formal method technologies do exist that would ease the development of avionics software.
Avionics
Ada Watch: Choosing the right Ada subset for strong static guarantees - Blog
August 13, 2013
While Ada offers many features that act as safety guards at run time, by raising exceptions when a violation is detected, some of these features may be too complex to guarantee a safe execution before the program is run. This is the case for example of pointers, which may be used to create arbitrarily complex shared data structures in memory. SPARK is a subset of Ada that forbids these features, most notably pointers, in order to be able to provide strong guarantees at compile time. A preview of the next revision of SPARK called SPARK 2014 is already available, as well as the associated verification tools.
Articles 1 - 2
