3 ms·
I would have expected them to use formal verification tools in the vein of TLA+ and such... or maybe use ADA for mission critical systems? But they only mentio
by naringas 6y ago
I would have expected them to use formal verification tools in the vein of TLA+ and such... or maybe use ADA for mission critical systems?
But they only mention Astree[1] which seems to be a propietary analyzer for C code
[1] https://en.wikipedia.org/wiki/Astr%C3%A9e_(static_analysis) https://en.wikipedia.org/wiki/Astr%C3%A9e_(static_analysis)
- Denvercoder9 6y agoIt's just a bad article. The whole section about Astree is based on a quote on HN about the ATV, a European resupply craft developed 15 years ago that has absolutely nothing to do with SpaceX.
- dahfizz 6y agoTLA+ is basically an academic tool. It allows you to verify your specification, but it is useless to detect bugs in your implementation. In my experience, the process of writing your specification in TLA is a buggy enough process to make it all a waste of time.
- superqd 6y agoNo, not just for academia. Apparently, Amazon uses it to check their designs for correctness. https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
- im_down_w_otp 6y agoI would have expected them to use SCADE, but given their choice of stacks that are entirely unverifiable, due to a combination of their complexity and their semantics, I can only assume that "control panel" was basically decorative, and that actual critical functions and alerts were handled by something with much, much higher safety assurances.