I guess the automated test suite just got larger. Testing all approaches on all runways on all airports worldwide...
Even most (not all, but almost none for meaningful applications) computer program cannot be proved to come to an halt [0], so complete testing is impossible by essence. We can only use more restrictive rules for programming but cannot formally guarantee anything.
As those systems are tied to the physical world, a whole lot of complexity is added by uncontrolled parameters.
Yet we love testing things. So a lot of techniques exist, such as SIL [1] and HIL [2].
So you could imagine using a real dashboard hooked up to a plane simulator. Which would enable testing the device in a wide array of conditions.
[0] https://en.wikipedia.org/wiki/Halting_problem [1] https://www.quora.com/What-is-Software-in-the-Loop-SIL [2] https://en.wikipedia.org/wiki/Hardware-in-the-loop_simulatio...
That is not true. If you can demonstrate that every loop or recursion is bounded, then the program must halt as a necessity. Loops of the form for (i = 0; i < N; i++) are trivially bounded, unless you're resetting i in the loop. If you have containers that are not being modified in the loop, the finiteness of your data structures is usually sufficient to form the lemma that the loop will terminate.
Recursive datastructures (such as cyclic graphs) are much more challenging to prove, and most challenging are fixed point algorithms (do { } while (changed);), as will be noted by them frequently being the causes of actual infinite loops in my experience. But if you had mandatory annotations to declare lemmas for termination, it is doable. With that feature, a programming environment that forbade you from writing code that couldn't be proven to terminate is probably sufficiently feasible to allow you to write large, complex applications.
"In cooperation with the University of Iowa and Rockwell Collins, this research focuses on the verification of safety properties on Lustre pro-grams. SAT or SMT, based verification approaches such as k-induction give good results on programs with a mostly discrete state space (boolean, bounded integers). However, when numerical computations are involved (real/float computations) the formalization of the property to be proved often needs to be strengthened using auxiliary lemmas to make it inductive with respect to the system’s transition relation. When attempted manually the discovery of such lemmas is time consuming and hinders the efficiency and scalability of formal verification. Automating lemma discovery hence appears crucial to allowing end-users to apply formal verification on industrial cases."
Taken from [0]
The seminars I attended to, from the creators of coq (a formal verification language), didn't disagree with this point of view. Of course, formal verification is not the only thing we can do [0].
In any case, what you propose seem interesting, if the halting problem was the only problem to solve to have a formally proven system.
[0] http://www.aerospacelab-journal.org/sites/www.aerospacelab-j...
There's about 20k commercial airfields, if you ran 20mins of simulation for each one then you're done within the year. Presumably Boeing can run in parallel and above realtime.
Are their watchdog systems for everything, or do they primarily rely on pilots noticing problems?
Wild speculation: Perhaps it's a power issue, something about the conditions causes a power demand that exceeds specs (or makes an LED? voltage drop too low). What else links all the screens?
But that is the nature of testing in multivariate conditions: e.g. if the bug triggers only when the heading is exactly 270.0000, I could see why a testing suite wouldn't catch it.