4 ms·
Is designing several independent systems (at least three, for voting to work) more or less expensive than formally verifying a single system?
by panic 11y ago
Is designing several independent systems (at least three, for voting to work) more or less expensive than formally verifying a single system?
- azeirah 11y agoThere's an important difference between a formally verified system and redundant systems however. At least, I think so! A formally verified system is verified "software". Different parts of a redundant system may rely on different parts of the hardware. If some hardware fails, a redundant system can still succeed, while a formally verified system is likely to fail.
- panic 11y agoGiven some model of the way circuits work, it's possible to formally verify hardware as well. Maybe your model doesn't quite match reality and your system will still fail. But redundant systems can also experience simultaneous failures of their components. It would be interesting to know which approach is more effective.
- chriswarbo 11y agoFormal verification is incredibly brittle WRT requirement changes (one of the sources of problems mentioned in the article). There are compromises, of course; eg. a small, verified answer-checker, which we can use to select correct answers from a collection of unverified implementations.