Re:F’: Flight Software and Embedded Systems Framework
by pjmlp on Saturday February 20, 2021 @04:42AM
(#26202960)
This is one of the reasons why NVidia went with Ada/SPARK for their security critical firmware project.
Re:F’: Flight Software and Embedded Systems Framework
by sterlind on Saturday February 20, 2021 @05:57AM
(#26203249)
iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and statically verify complex preconditions and postconditions.
I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.
Re:F’: Flight Software and Embedded Systems Framework
by pjmlp on Saturday February 20, 2021 @06:09AM
(#26203303)
Yep, here some very good books about it, specially relevant given the main subject.
"Building High Integrity Applications with SPARK"
https://www.amazon.com/Building-High-Integrity-Applications-...
"Building Parallel, Embedded, and Real-Time Applications with Ada"
https://www.amazon.com/Building-Parallel-Embedded-Real-Time-...
"Embedded Software Development for Safety-Critical Systems"
https://www.amazon.com/Embedded-Software-Development-Safety-...
There should be an industry push for certified Rust tooling, it would save the aerospace and auto industry billions. Or you could use the unsexy but also very good ADA 2012, which is already certified.