David Lesens from Astrium was a member of the Hi-Lite project ("was" because the project is finished now, see the previous post), and has tried GNATprove - the formal verification tool for SPARK 2014 -  on space vehicle software as an industrial case study of the project. And it turns out GNATprove performed pretty well!

Together, we submitted a paper to the conference DASIA 2013 - it seems to be the main meeting place of industrials in the space business. In any case, all the talks presented satellites, missions going to Mercury, launchers ... Quite impressive.

SPARK 2014 is a major upgrade of the SPARK technology, now based on contract based programming as it has been added to Ada 2012. It supports a large subset of Ada including generics and discriminant records.

David has put the technology to use during the three years of the project. The case study is an interpreter for a language that is used for on-board control procedures, and it is called OBCP. It uses generics, discriminant records, tagged types and many Ada 2012 features such as preconditions, postconditions, large case expressions and quantified expressions. In fact, using all these features extensively, David in effect put the technology to quite some stress test. Many improvements of the technology are in fact due to his problem reports and suggestions. In the end, GNATprove performed well on his case study, even though a few issues remain to be solved.

Thanks David for his contributions to the project, and if you want to try SPARK 2014, you can download the GPL version of GNATprove at the libre site.