The 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.
[…]
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 than to convince yourself of the fact that switching a light switch turns on the light. Indeed the multiple whiteboards of proof included many skipped steps, skipped because they were too tedious to go into formally. Many steps were reached using the long-cherished method of Proof by Induction, others by Proof by Reductio ad Absurdum, and still others using Proof by Graduate Student.
For our homework, we had to prove the converse: if the light was off, and it’s on now, prove that you flipped it.
I tried, I really did.
I spent hours in the library trying.
After a couple of hours I found a mistake in Dr. Zuck’s original proof which I was trying to emulate. Probably I copied it down wrong, but it made me realize something: if it takes three hours of filling up blackboards to prove something trivial, allowing hundreds of opportunities for mistakes to slip in, this mechanism would never be able to prove things that are interesting.
https://www.joelonsoftware.com/2005/01/02/advice-for-compute...
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...
By the end of that summer of 1983, Richard had completed his analysis of the behavior of the router, and much to our surprise and amusement, he presented his answer in the form of a set of partial differential equations. To a physicist this may seem natural, but to a computer designer, treating a set of boolean circuits as a continuous, differentiable system is a bit strange. Feynman's router equations were in terms of variables representing continuous quantities such as “the average number of 1 bits in a message address.” I was much more accustomed to seeing analysis in terms of inductive proof and case analysis than taking the derivative of “the number of 1’s” with respect to time.
http://longnow.org/essays/richard-feynman-connection-machine...
https://www.youtube.com/watch?v=SVRiktFlWxI#t=2h9m38s
Software could be proven correct, but we abandoned that, just gave up on it, it’s too hard. But we can test it. We can use science, and we can write tests that demonstrate that the software is not failing. We treat software like a science, not like mathematics.
— Robert Martin
So one trick is to work on DSLs with restricted semantics that are good enough for your domain. That makes proofs plus other formal techniques, and hence security guarantees, much much easier.
But if you insist on Turing complete languages, as I explained above, you can e.g. build abstract interpreters or data flow analyses that are able to prove really sophisticated things. I have implemented a C abstract interpreter for an industrial client that among many other things detected whether you were making potential out of bounds accesses to arrays, or potentially using uninitialized pointers. Of course it erred on the safe side. But it was really precise (few false positives). Not a walk in the park as it relies on Galois connections. See the seminal Cousot & Cousot 1977 paper [1].
> The fly-by-wire flight software for the Saab Gripen (a lightweight fighter) went a step further. It disallowed both subroutine calls and backward branches, except for the one at the bottom of the main loop. Control flow went forward only. Sometimes one piece of code had to leave a note for a later piece telling it what to do, but this worked out well for testing: all data was allocated statically, and monitoring those variables gave a clear picture of most everything the software was doing. The software did only the bare essentials, and of course, they were serious about thorough ground testing.
> No bug has ever been found in the “released for flight” versions of that code.
so not quite that tests are useless because blackbox, but more that yes, it is possible to write software that facilitates showing a code will do what it says it will do.
In another note, I do feel sorry for the engineers but at the same time Airbus also has similar MCAS system, but the only thing that saves them is an extra Angle-of-Attack sensor whereas I believe the boeing relied on just one or two. Airbus had 3 AOA sensors and if 2 agreed, that was the data fed into the MCAS.
It still boggles my mind that they would place a bigger engine when the original plane was not built for it at all, this was 100% profit orientated move to prevent Airbus from taking Boeing's majority marketshare, it's highly ironic that the opposite results.
Even more infuriating is that Boeing passed it off as the exact same plane, not much extra training is necessary, along with FAA giving their blessing, now caught up in the mess.
Canada for instance is now looking to the EU for an independent auditing, as any credibility FAA has built up over the past years has taken a significant hit.
Note however that there were several software-related crashes in the early days of Gripen. Might not be related to exactly this code, but to the problem of regulating the feedback loops to manage the plane's purposeful instability
Off topic but here's a neat youtube video of Gripen jets undergoing rapid turn-around, on a normal street road with just a handful of people, and special tools for the crew:
Second crash (over middle of Stockholm) https://youtu.be/mkgShfxTzmo?t=133
From Wikipedia: During the test programme, concern surfaced about the aircraft's avionics, specifically the fly-by-wire flight control system (FCS), and the relaxed stability design. On 2 February 1989, this issue led to the crash of the prototype during an attempted landing at Linköping; the test pilot Lars Rådeström walked away with a broken elbow. The cause of the crash was identified as pilot-induced oscillation, caused by problems with the FCS's pitch-control routine.[22][33][34]
In response to the crash Saab and US firm Calspan introduced software modifications to the aircraft. A modified Lockheed NT-33A was used to test these improvements, which allowed flight testing to resume 15 months after the accident. On 8 August 1993, production aircraft 39102 was destroyed in an accident during an aerial display in Stockholm. Test pilot Rådeström lost control of the aircraft during a roll at low altitude when the aircraft stalled, forcing him to eject. Saab later found the problem was high amplification of the pilot's quick and significant stick command inputs. The ensuing investigation and flaw correction delayed test flying by several months, resuming in December 1993.[22]
the second was even more shocking, all of a sudden it looked like he was trying a Cobra maneuver until he ejected! that's insane.
I like really long function bodys so I get turned on by the idea.
That's extremely different to a system that silently severely mistrims you, then tells you to disable your ability to trim electrically before you can fix the mistrim, as if that even makes sense, all while overpowering the yoke with aerodynamic load.
For the record, Airbus's three sensors haven't prevented crashes completely. Here's one where two sensors were damaged, causing the correct sensor to be treated as erroneous and lose the quorum vote:
https://en.wikipedia.org/wiki/XL_Airways_Germany_Flight_888T
MCAS performed as designed. Only reading one AoA sensor, acting on bad readings, not rejecting values that are clearly out of bounds, operating continuously without any limits on its pitch authority, all of this was how is was designed to work. You could have proved MCAS “correct” and ended up with the exact same result.
A lot of software problems are due to discrepancies between the design and the implementation, of course. But it’s not a panacea.
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.
However, this looks like an unusual case. Based on the fact that they had such a dumb design for this system, that shouldn’t have passed muster in any aviation context no matter your software methodology, it’s probably not representative enough to draw a larger lesson about engineering. The larger lesson seems to be business and regulatory.
Regarding Japanese cars, Toyota went through a big thing with unintended acceleration that got quite a few people killed. Software was suspected, but the cause was ultimately determined to (mostly?) be a combination of drivers mixing up the accelerator and the brake (happens more often than you might think) and unsecured floor mats pushing the accelerator down. I bought a Toyota not too long after this and the dealer made a special point to show me how the floor mat attached to the floor and that I must be sure it was solidly connected.
Their software was audited and apparently it was really badly made. It was described as “spaghetti-like” and had global variable abuse, ignored errors, failed to restart unresponsive tasks, and had potential memory corruption problems. It’s quite possible that this really was the cause, and a jury even found this to be the cause in a civil trial over one of the crashes, but it was never definitely linked.
How do you solve it? Assume your AoA sensor is always correct? Congratulations, MCAS is a provably correct solution! Make the sensor behavior more complex? Sorry, the problem is now intractably complex (and still doesn't model the actual hardware).
You could write a formally verified MCAS system in Coq or whatever that still kills people because you didn't consider the case of sensor failure (because that wasn't in the requirements). Or because you didn't consider the case of double sensor failure or a combination of extremely rare hardware failures (that wasn't in the requirements either!).
Your code is mathematically perfect, yes! But it was built with the incorrect assumption that the hardware is perfect as well!
I'll take a robust set of tests written by someone thinking outside of the box in terms of what could fail, how it will be used in operation, etc. over a piece of software "guaranteed unsinkable" because it is formally verified.
A necessary part of why types are so useful is that understanding the types is easier than understanding the code itself.
If the types become so complex that they start to get harder to understand than reading your code (e.g. C++ template errors can sometimes get this bad), then they are no longer helpful.
https://en.wikipedia.org/wiki/Correctness_(computer_science)
In science nothing can be proven but in the world of logics and math, things can be proven. Bugs can arise where programs intersect in the real world.
However, because we don't do proofs in software, there are bugs.
Edit: that said, spending the formal spec time will probably reduce the number of bugs far below than what we find normal now. But money...
Well, the context is flight control software for airplanes. If that code is bug-free but doesn't intersect the real world, that's rather useless. And if it intersects the real world but therefore is not bug-free, that's not a great argument for proofs of formal correctness.
But all of that is kind of beside the point. The MCAS specification was the wrong thing. Proving the implementation correct is useless. (You asked what is a bug in a spec? MCAS shows you the answer. Only taking input from one sensor is the wrong thing. Repeatedly applying nose-down is the wrong thing. It seems like I'm missing one or two more.)
The system which should have been using for attitude detection in the 737 MAX, and wasn't.
Man: Doc it hurts when I bend my knee this way.
Doc: Well don't do that.
EE: The hardware state machine runs into the weeds when given these inputs.
Tech Rep: Yeah don't do that.