|
|
|
|
|
|
by jnash
1554 days ago
|
|
|
It is a lot easier to get the spec right than getting the implementation right. > How seL4 or CompCert protect me against against hardware issues like ECC errors, or the Pentium FDIV ? That's a straw man argument. Nobody claims that formal proofs can protect you from hardware failures. However formal proofs can protect you against Pentium FDIV style bugs (see ARM formal specification efforts). Intel started massively investing in formal proof methods because of the not-formally-proven-correct Pentium FDIV fiasco. |
|
|
In real world use, and other than in academic contexts, is of reduced usefulness that I claim my component used TDD and was formally verified, while throwing over the wall, the responsibility of delivery for a system that can't fail, to somebody else.
So my claim is, we don't know how to do it, we can formally verify some components, and we hope the spec is correct.
Forgetting the spec only has the known known's and unknown known's, but not the unknown unknowns, is a kind of intellectual hubris I am not willing to bet lives on. Certainly not under the disguise of using formal methods.
So I am referring to examples like this:
"A380 Flight Controls overview" [1]
• 3 PRIMary Flight Control and Guidance Computers integration of Auto Flight (ex FGEC) and Flight Control (ex FCPC)
• 3 Auto-Pilots
• 3 SECondary Flight Control Computers dissimilar Software and Hardware, simpler Control Laws
[1] https://www.fzt.haw-hamburg.de/pers/Scholz/dglr/hh/text_2007...