Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers

Re:Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers by posix_me_less on Saturday June 29, 2019 @01:05PM (#20313609)

If so, this may be a good back-to-reality counter-example for all the over-zealous formal proof enthusiasts. There is an old paper from 70's by people who designed complex systems where they stress the point that even if your system was designed and formally checked and if it obeys all the known rules and specifications, it will still fail in real world unless you test and iterate it a lot. Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. One has to experiment/iterate to find the very specifications that are then going to be designed against. Which in 737Max case was seemingly neglected.

[ Parent | on HN ]

Re:Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers by mannykannot on Tuesday July 02, 2019 @11:58AM (#20336379)

> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real.

You cannot exhaustively test software either - the number of cases to cover are beyond astronomical.

The effectiveness of both specification and testing ultimately depend on the same thing: thinking of all the relevant possibilities. If you overlook a possible failure mode, there's no guarantee it will be caught at any phase. The main benefit of formal methods, I think, is that the rigor tends to make such oversights visible.

the only people who think formal methods are a magic bullet are those who have not tried them. Likewise, the only people who think more testing (and especially unit testing) is a magic bullet are those who don't understand combinatorial complexity.

[ Parent | on HN ]

Re:Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers by hobofan on Saturday June 29, 2019 @01:18PM (#20313661)

> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real.

Is that so? Wouldn't it be in theory possible to verify it against our current understanding of all laws of physics and the corresponding equations?

[ Parent | on HN ]

Re:Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers by posix_me_less on Saturday June 29, 2019 @01:52PM (#20313843)

You are forgetting nondeterministic aspects. Only in theory, aircraft and atmosphere is a deterministic Newtonian machine, in practice, less so. But even if so, physics simulations can't be done and evaluated for all possible initial conditions for even the simplest model.

One can imagine a mental model of airplane and make a formal design for it. Then do a formal check in the most important scenarios that introduce weather, human action, system failures. The design will always fail for some scenarios. Not a problem if those are not important (in terms of risk). But which scenarios are the important ones? Probability and severity of consequences of those scenarios are much needed knowledge, and one can find those only via the good old method of iterative testing in wild.

[ Parent | on HN ]

Re:Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers by ori_b on Saturday June 29, 2019 @03:17PM (#20314239)

But it obeys the laws of physics perfectly as it nosedives into the ground.

[ Parent | on HN ]

Re:Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers by nutjob2 on Saturday June 29, 2019 @01:25PM (#20313689)

It also has a user interface. Are you saying it's possible to formally quantify human behaviour as well?

[ Parent | on HN ]

Re:Boeing's 737 Max Software Outsourced to $9-an-Hour Engineers by hobofan on Saturday June 29, 2019 @02:51PM (#20314117)

Every program has a inputs, and with that some more ore less direct version of a user interface. You define the acceptable input values and then define what happens with unacceptable ones (and same for combinations).

If that were not verifiable, then no program would be.

[ Parent | on HN ]