Those processes are expensive. It'd imagine that they're a huge political problem to maintain, giving cost-cutting pressures and the temptations of COTS [1].
[1] https://www.faa.gov/aircraft/air_cert/design_approvals/air_s...
So it all makes me wonder about the official maturity of Boeing's 737 team, and also how much that rating relates to actual software quality and safety objectives (as apparently achieved in the space shuttle work)....
My original point was that flight critical software shouldn't be lumped in with the bugs-typical world of software. I still say that's correct.
But "bug" has a range of meanings. From what I read of the story of the original fatal error on the 300 MAX, the software was not buggy in the sense of "deviating from specification". It's just that -- as it turns out -- the specification was bad, and the MCAS should not have overridden pilot input when it did.
In a sense -- the one I consider most important -- that matches my model of flight-critical software. As software, they made absolutely sure that, in every case, it did what it was intended to; to the extent that it was in error, it was not in the sense of "we failed to make the software do what the spec says".
OTOH, I agree that "bug" is taken more broadly in software than the sense I was using here, that there usually isn't such a clean ("Waterfall") separation between "specifying what the software should do" and "ensuring that it does that" -- there's a collaborative process of ferreting out the implications of "what the system should do at what points".
In these latest events, it looks like the bug was in the narrower sense I meant above, of "it doesn't meet the spec", and that bug was found before deaths. From the article:
>The problem was that an indicator light, designed to warn of a malfunction by a system that helps raise and lower the plane’s nose, was turning on when it wasn’t supposed to, the company said.
Now, in fairness, that's a much later discovery than my optimistic model held, but still far earlier than "being used for flying the public around", as (the analog of) might happen with the software industry more generally.
What is worrying is that there could be many other potential sources of failure which simply didn’t trigger because the MCAS situation was so bad it led to 2 plane crashes before they even had a chance to bring down some planes.
In other words, if you have 2 bugs, one with a 1/100 chance of triggering and the other with a 1/1000 chance of triggering, by the time you hit 500 attempts, odds are the first bug triggered twice, while the second didn’t even once. So you solve the first bug, that still leaves you with a problem that has a 1/1000 chance of triggering, when the expectation is that bugs should only trigger at worst 1/10000 times.
Solving the MCAS issue is not by itself a reliable indicator that this is a safe plane to fly, especially since we know there are many fundamental procedural reasons to be worried about the quality of the plane.
The entire purpose of MCAS was to override pilot input as the typical instincts of a trained 737 pilot is to do the wrong thing. The failure was not handling edge cases (conflicting or missing sensor data) and no clear way to turn off the system when it was failing.
Testing is not only not enough, it's also not required :) (as Dijkstra said, it can only show the presence of bugs, not their absence)
For example, the software for some automated subways in France has never been tested, only proven correct (source: https://www.youtube.com/watch?v=jc9QmqKIUj4&t=54m50s).
Similar formal methods are used for critical software pieces in Airbus aircrafts (source: the same speaker as for the linked video, but I don't remember which talk that was in).
But I guess (again) that having formal specs getting proven helps to avoid inconsistent specs. I recall a talk by Martyn Thomas where he said that with these methods it was harder to get programs to compile (for example, the compiler could complain if it detected an inconsistency, either between the spec and the program or within the spec itself).
