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.
[ Parent
| on HN ]
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-...