"Various hacks (as we would call them in the software industry) were developed." Dear God. That's a sentence I never, ever wanted to hear about an aircraft.
The modern 737 is a collection of hardware and software hacks, flying in close formation.
How the Boeing 737 Max disaster looks to a software Developer
41–50 of 306 posts
Re: How the Boeing 737 Max disaster looks to a software Developer
#42The irony of software is that it is the only discipline in engineering where results can be proven with logic. Yet we still do testing on it as if it was a blackbox.
I refer you to Joel Spolsky about formal proofs of programs: […] So in the first day of that class, Dr. Zuck filled up two entire whiteboards and quite a lot of the wall next to the whiteboards proving that if you have a light switch, and the light was off, and you flip the switch, the light will then be on. The proof was insanely complicated, and very error-prone. It was harder to prove that the proof was correct th…
I have a MSc in formal methods, and this is really misleading. Surely you cannot make some proofs easily. However, how did Airbus verify that some errors simply do not exist in their fly-by-wire software (which is ~100 KLOC implemented in a subset of C)? (I'm sure Boeing also employs these techniques internally).
Using abstract interpretation. There are tons of formal methods, ranging from type systems to formal proofs. Lots of compromises can be made to make them practical and useful for a particular domain. Look into [1,2] for some quick introductory examples. Going straight into formal proofs is in general a really bad idea.
I have worked on railway control systems, with really nasty potential race conditions and managed to prove the absence of large classes of errors. Then derived implementations formally. It's really not that hard. There's even a subfield of CS looking into verifying formal properties of biological systems [3], which are really complex.
[1] http://adam.chlipala.net/frap/
[2] http://www.concrete-semantics.org/
[3] http://lucacardelli.name/Papers/Abstract%20Machines%20of%20S...
Re: How the Boeing 737 Max disaster looks to a software Developer
#43> In the 737 Max, only one of the flight management computers is active at a time—either the pilot’s computer or the copilot’s computer. And the active computer takes inputs only from the sensors on its own side of the aircraft.
Also wondered what was the logic behind this decision...
Like everything else, they were maintaining certification. The original avionics worked that way. The same reason that the LCD screens display simulations of the original avionics hardware such as the artificial horizon.
Re: How the Boeing 737 Max disaster looks to a software Developer
#44What a stellar example of an article on a complex topic written to be clear enough for the audience to understand. I especially like the way he brought it back repeatedly to hands out the window and bitey dogs.
I also heartily agree with him that software's general laxity with regards to reliability is contagious. I've come think that calling it all "software" is dangerous, like thinking of all things made with atoms as the same. I think we as an industry should get together, divide the work into various domains, and establish professional and ethical standards for the domains that matter. Standards with teeth, such that de…
Something like (or exactly) software systems safety methods should be applied to critical systems (such as aircraft systems). DoD does this for all of their critical software. And I say "something like" only to indicate there may be something particular about software in aircraft. I doubt it though. And as the article indirectly points out, analysis was severely lacking.
DoD Software System Safety handbook https://www.acq.osd.mil/se/docs/Joint-SW-Systems-Safety-Engi...
Full disclosure: The company I work at does this type of work. I don't work in that group.
Re: How the Boeing 737 Max disaster looks to a software Developer
#45Earlier quoted context omitted.
Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.
I think this is likely to be true, but I do wonder if there might be a better way to spend those resources. For this particular example, you’d have been better off putting more money into flight testing with various sensor errors.
Well, yes. But, and who knows if it is true, but you would think you can think up that you need sensor errors to be tested and maybe figure out you need three errors vs two for instance to cover all cases; formal systems can help you model and reason about that and come up with cases that are not covered.
I think the point is which these disasters show, and some others in the past (was there not a recalled Japanese car with a software issue?) that a few million more for the right resources will save you a lot more down the line. Problem is that this is not really a statement we can prove for formal verification because we do not have enough to compare with; i have a very strong feeling it will make quite a significant difference; if not for the proofs themselves then for the sheer number of hours and time the proofwriters thought about it by the time of delivery.
Re: How the Boeing 737 Max disaster looks to a software Developer
#46"Various hacks (as we would call them in the software industry) were developed." Dear God. That's a sentence I never, ever wanted to hear about an aircraft.
The modern 737 is a collection of hardware and software hacks, flying in close formation.
cloud formation*
Sorry, I couldn't resist.
Re: How the Boeing 737 Max disaster looks to a software Developer
#47"Various hacks (as we would call them in the software industry) were developed." Dear God. That's a sentence I never, ever wanted to hear about an aircraft.
The modern 737 is a collection of hardware and software hacks, flying in close formation.
> flying in close formation
"conveniently in close proximity most of the time, usually".
I wonder what the equivalent of "Developing in Production" looks like for planes, or if this is it?
Re: How the Boeing 737 Max disaster looks to a software Developer
#48What a stellar example of an article on a complex topic written to be clear enough for the audience to understand. I especially like the way he brought it back repeatedly to hands out the window and bitey dogs.
I also heartily agree with him that software's general laxity with regards to reliability is contagious. I've come think that calling it all "software" is dangerous, like thinking of all things made with atoms as the same. I think we as an industry should get together, divide the work into various domains, and establish professional and ethical standards for the domains that matter. Standards with teeth, such that de…
We already have standards, one of which is clear technical documentation of the system, which the users were not getting. Also we have standards for writing fault tolerant systems (I would say even 2 measure devices are not enough, you need at least 3 to be able to decide).
In Boeing it's clear that software best practices and standards were not followed at all.
As an example here's the description of the Google Test Certificstion process:
Re: How the Boeing 737 Max disaster looks to a software Developer
#49 I believe the relative ease — not to mention the lack of
tangible cost — of software updates has created a cultural
laziness within the software engineering community.
As someone who carefully crafts their code to strive for perfection, seeing sloppy work out there in the wild drives me nuts. I know folks here will deride me for being "inefficient", but in the long term I still maintain from my experience it's less efficient to push out buggy software and try to fix it retrospectively.
Re: How the Boeing 737 Max disaster looks to a software Developer
#50The irony of software is that it is the only discipline in engineering where results can be proven with logic. Yet we still do testing on it as if it was a blackbox.
Proving that software matches the spec is one thing, proving that the spec is free of bugs is quite another.
Indeed. It is normal that implementation will find a bug in the spec. Anecdotally, have never found a flawless RFC. Every real-world implementation of an RFC I've ever done has found some discrepancy when it came to compatibility testing.