Boeing identifies new software problem on grounded 737 Max
bloomberg.com
bloomberg.com
Bugs in software happen because situations where they arise are sometimes hard to predict. You can test your software all you want but it's not until it's in the field that you start discovering new issues because people tend to do things in ways developers didn't consider.
Tesla's software has over a billion miles of data on it and it still has issues in some basic functionality. And let's not talk about Iowa which in itself was a major failure in software release management.
Assuming that's not hyperbole and just to be pedantic:
mov ax,cs
mov ds,ax
mov ah,9
mov dx, offset Hello
int 21h
xor ax,ax
int 21h
Hello:
db "Hello World!",13,10,"$"Expected: "Hello, World!"
Actual: "Hello World!" (missing comma)
See spec: https://en.wikipedia.org/wiki/%22Hello,_World!%22_program
MCAS used only the one sensor, this decision made so as to avoid recertification.
http://www.b737.org.uk/mcas.htm
“Are we vulnerable to single AOA sensor failures with the MCAS implementation or is there some checking that occurs?”
https://www.aviationtoday.com/2019/11/02/boeing-ceo-outlines...
That's not really true. The airframe is fine, except it doesn't handle like a 737. MCAS was meant to make the MAX handle like a 737.
Mentour Pilot, a 737 instructor with a youtube channel, has covered this fairly extensively: https://youtu.be/TlinocVHpzk?t=951
That's fine, but know that the way you're choosing to use the word "unstable" doesn't square with how it's actually used in the aviation industry.
So far only one "aircraft" has had perfect software, and that was the Space Shuttle, every single other aircraft out there has had software issues that are worked out over the life of the aircraft, just like every piece of software, even that which has very strict testing regimes, has had defects in it.
Actually it had 3+ known bugs.
Will probably be optimized out by a modern compiler though. Sad.
With all of these aircraft that are so computer reliant it becomes this magic box that is nearly impossible to diagnose and fix quickly. You do the circuit breaker reset, then reset the whole jet, then check the connectors of the components of the system, then change some of the computers/controllers, all the while checking for any fault code that might lead you down the right path.
This process often takes 30-60 minutes by which time you’re boarded and ready to go and if it’s not fixed by then it turns into getting everyone off the aircraft and finding a different aircraft so the broken ship can be taken to the shop and a through investigation of the issue can be done.
Meanwhile the customers riding in the MD88 already had their mechanical part replaced and they’re on their way, none the wiser because the mechanic got it diagnosed and replaced before boarding was even done.
Part of me feels like many of these companies don’t keep code secret to protect IP, instead they do it because they know it’s a burning train wreck and don’t want people to find out.
https://www.safetyresearch.net/blog/articles/toyota-unintend... https://users.ece.cmu.edu/~koopman/pubs/koopman14_toyota_ua_...
Thanks for posting that. That was a horrifying read. I'm at a loss for words.
Looks like I've got some more reading to do...
- "No configuration management"
- "No bug tracking system"
- "No formal specifications"
- "9,273 – 11,528 global variables"
- "Uses recursion, no mitigation for stack overflow. Memory just past stack is OSEK RTOS area"
I thought of Toyota as a much better company in terms of safety and reliability. I can't imagine other manufacturers and their code.
Another is the race conditions. Unless toyota/denso is very stupid, I really doubt than more than one thread is running on the CPU, because automotive OSEK typically run in locked step mode, meaning everything is run in one sequential thread, even if there are several cpu core.
Thirdly, global variables, as there is just one thread, are a perfectly ok thing to use, provided you add a special thing in the OS which guarantees that all inputs are frozen when a block of functions are called.
It is a very orientated slideshow with unproven claims, he discredit himself.
It's a bad barrel: a company that has, on a cultural level, put its business motive above its responsibility to deliver a safe and high-quality product. We have seen documented evidence that employees knew there were dangers and problems, and discussed these issues, but nobody cared enough to slow things down and get the product right.
Good point about whistleblowing. Perhaps the faas reliance on self regulation alsobplayedbibto that consolidation, so even the one other place they might have gone was just something that looped right back to the monolith.
I suspect that a thorough review of some of the more complex Airbus airframes currently in operation would result in some similarly scary findings, tbh.
Any fuel-air explosive will do.
Thus the obvious solution to quality problems is to switch missile software engineers and aircraft software engineers, and encourage them not to care about quality.
So, they can't even name the mcas system anymore?
Which is probably a good thing, except for the part that it took hundreds of people to die first to get here.
You will note, some of these scenarios are essentially fuzzing the memory of the flight computer and seeing what happens, ideally most bit flips will either be detected or be minor, but some can end up causing issues. I'm not sure if it would be possible to explore all the branches in the software in any sort of reasonable amount of time.
Flight software development lifecycle--and regs as you point out--still needs to catch up.
I thought that the paris metro was the posterchild of formal verification methods.
It's a completely different experience that likely only a handful of modern testers would even contemplate nowadays, but has always been a shining example of something to aspire to be part of one day for me.
It isn't at all easy, and basically requires the discipline to understand, document, and justify every single line of code within the context of the overarching system.
No business wants to deal with it, and it is no surprise that only publically funded projects tend to get anywhere close.
https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/201100...
https://developers.slashdot.org/story/00/05/19/050258/space-...
Do you have a source for that claim ? I'm skeptical that even a testing process costing billions of dollars could claim to cover all possible inputs and states for a software system of any complexity.
"as perfect as human beings have achieved" != perfect
It's taken me a while to come to the realization that all project management is is a backlog manufacturing and prioritization layer that operates on top of actual software engineers.
Most just want to implement things, and don't care what it is they are implementing as long as they are getting paid.
Now if you're talking about features that don't touch these things, go nuts. And there lies a second issue: the identification and distinction between what stuff is "go nuts" and what stuff is "do it right the first time". You can't approach every project with the latter or you'll waste so much time in the design phase when really you should just throw your new CSS theme out there and see how it goes. But you just can't approach the "account creation" feature the same way.
And yes, corporations aren't people, corporations don't have morality, I've heard all those excuses. Those corporations are comprised of people and those people should not be held to a lower standard.
The 737 Max is much worse at doing things that were done much better for decades before it.
It's another matter entirely to pass on the flawed device to a third party with no preparations and warning. Then people die.
Given that attitude, it's no wonder 99% of software out there is utterly bug-ridden.
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...
But they are also super expensive.
And no one has any money to spend on anything like testing or quality any more.
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.
(I didn’t say anything about GP being wrong, I simply gave more details about the how and why)
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).
See MCAS programmers at $9/h.
> Increasingly, the iconic American planemaker and its
> subcontractors have relied on temporary workers making
> as little as $9 an hour to develop and test software,
> often from countries lacking a deep background in
> aerospace -- notably India.
Found it. Was Bloomberg. Here is the old thread.
Boeing has literally relocated their plant operations cross-country in the past in order to break the workers' unions.
Just think about how much pressure they can exert on a non-union profession like software development.
E.g. just to use a random example, Russian statistics show that the average pay of an architect is something like $800/month in many regions - in some more, in some less, but definitely well withing $9/hour; and for doctors in regions outside Moscow it's something roughly similar; Moscow seems to get something like 2200$/month in the average statistics so that's more than $9/hour if they're working sane hours.
I agree with you. However, if you're not some high level manager who controls this, what's the next best thing you can do?
I think most problems are less technical and are more about people and processes. You can still argue you don't have enough influence there, and that's completely possible and realistic. But that should be where we direct attention.
Yes, some technical advances in better tools and languages that provide stricter proofs and so on are needed and will help. But ultimately it's still the people that need to learn, use, and enforce the processes.
Gotta fundamentally disagree with you right there. We absolutely can make high-quality software with our current tooling. The issue is that doing that is expensive and time consuming, and the Market optimizes on good enough to be sold and not dropped.
This expense and difficulty isn't an inherent fault of the tools, but rather the monstrous other side of the coin in proving what your system isn't.
There are many implementations that are composable to generate an end result, the trick is to expend the energy to ensure you've made the specific one that also doesn't run into undefined behavior, domain specific or otherwise.
You will never escape from the tyranny of having to clearly communicate to a perfectly obedient machine exactly what it is you want it to do; part of which is being able to identify when you don't have all your requirements right.
Airbus has designed their planes to counteract bugs by adding tremendous amounts of redundancies. The Max is Boeing’s effort at creating an Airbus like plane without the redundantsafety features.
Unless we see fines based on a percentage of revenue or the CEO/Board of Boeing being thrown in prison, then we won’t see change.
But it’s not a real defense for the Max because the problem with the Max is that Boeing has shifted a lot of the work from hardware to software.
This defense only punts the ball a few yards because the question now is why Boeing chose to shift a lot of the reliability from hardware, which this defense admits is better engineered, to software, which it admits is almost intrinsically worse.
If anything, this defense leads to the conclusion that the Max is an intrinsically unsafer plane, because it has shifted far more of the burden to software which is an intrinsically worse engineering discipline.
If it was just a matter of the software QA being rushed then the additional time gained by the grounding of the planes could solve the problem. But if it is software engineering itself which is the problem then no additional time will help unless it leads to shifting some of the burden of safely flying the plane from software to hardware, which doesn’t even appear to be an option Boeing has considered.
[1] https://www.theregister.co.uk/2018/01/26/cloudflare_crashes_...
Because most of it is software anyway. Unless the CPU is something ridiculously simple, like an 8-bit microcontroler, a lot of the instructions are executed by microcode stored in ROM on the CPU. What those patches do is load a replacement software in RAM at boot time.
My dishwasher stopped working today. Last week I had to replace a wheel bearing in my van ($900). I just got a refund for a pond aerator that stopped working after a few weeks. And the head came off my plastic toy.
Hardware fails all the time: does that mean I can generically say all manufacturing has shitty QC?
This is so not true.
Processes? Like T-CMM/TSM, FAA-iCMM, ISO 90003, TCSEC, TSP, etc., etc.? Languages? Like Ada, MISRA, Modula-2/IEC1131, Cyclone, etc., etc.? Tools? Like FRAMA-C, MALPAS, SPADE, SPARK, TLA+, etc., etc.?
The simple fact of the matter is that we've had all the processes, languages & tools to write high-reliability, secure code for decades. Go check out the CMU SEI for how long that one institution has been trying to get people to do the right thing.
The joke is that the software industry by and large wants to pretend we don't, and claim that there's some magical new tech that needs to get invented and when it arrives everyone will jump on it and suddenly software bugs will be a thing of the past. And every new tool, tech or whatever that shows up re-proves some unpleasant basic facts: writing secure, provable, reliable code is time consuming, usually difficult, which translates to relatively expensive. And the software industry doesn't want to hear that, or invest in it, and excuses it's miserable security record with "it's not us, the tech doesn't exist to do the job right".
As a sidenote, this is why I have a visceral distaste for the Rust people (the language seems fine). If they'd spent those (presumedly) thousands of man years building on and improving Ada instead of being all NIH averse we'd be much further down the road. They could have participated in the process and gotten their wish list included in the Ada-2012 standard and built on 35+ years of experience. But, hey, it's more fun to start from scratch every decade or so.
So they did not do enough testing before, just the happy case and never considered sensor failures. I am now wondering if they tested the rest of the software or FAA will just look into MCAS and ignore all the rest.
Why didn’t they find these bugs during the plane’s development and certification? It appears the testing then was less rigorous. They should extend the same rigorous testing to their other aircraft models also.
I do see an opportunity for software that ensures you are only booking journeys on the aircraft you feel are safe.
Ahh, "we'll ship it when it's ready, not on some arbitrary deadline." Music to any engineer/builder's ears.
https://en.wikipedia.org/wiki/Fault_tree_analysis
Basically, you should be designing every system to gracefully handle the failure of every other system on which it is dependent.
So the MCAS routines, if they had been done correctly, and properly classified as to the hazard level, should have taken into account failures of the Flight Computer they were running on, anomaly detection via cross-check with the second AoA vane, etc. That quite clearly did not happen.
The same approach applies with any other hardware/software integration. Your sensors will break. You therefore need to determine what you need to do when that happens.
Yes, electronics fail in the most weirdest ways due to connector failures, RF interference, software error, sensor failure.
When my systems start failing or acting up due to improper stabilization PID gains, etc. I have a big switch for MANUAL mode. I am able to fly this thing as long as the servos, radio, and camera get power. All sensors could be sheared off. I have no idea what my airspeed is ever because I don't use pitot tubes so I use a known engine throttle % whose stall characteristic I understand for level flight in various wind conditions and I don't make sudden maneuvers at throttle below this point.
Fixed wing planes have remarkable aerodynamic stability and I don't understand why 737 MAX cannot be piloted in a fly by wire manner with all computer aids disabled, giving the pilots direct control of the servos with a big red switch that mechanically disconnects the flight computers. This requires almost no code to implement.
The pilots do have direct control over the stabilizer trim, and have always had the ability to disable the electronic system in case of stabilizer trim runaway. This was not new to the MAX, and would have effectively disabled MCAS.
Reading comments such as:
> 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.
Implies that there is intrinsically some computer system that continually parses the commanded stick deflection and applies an overlay.
What I am suggesting is a single toggle to make everything shut up and reset all servos to their midpoint all at once in one shot and let the pilot just fly the plane.
I have not seen any evidence that such a system exists. It is the elephant in the room. Airplanes do not need complex electronics to just fly if they are aerodynamically stable, and this plane is more or less stable except that under some conditions it will make the pilot soil their pants at higher AoA, which is where the promises of MCAS come in. Big deal. They can mentally compensate against that manually better than fighting a computer system working actively against your commanded inputs.
I have experienced the joy of a badly tuned PID controller turning my stabilization system into involuntary high speed descent. The fix is always to tell the computer to shut up and just fly the plane 100% manually.
That's not how the 737 works. The 737 is not a fly by wire aircraft. The pilots control the rudder, ailerons, and elevators electrohydraulically; there is no computer filtering. The electric stability trim system, which is what MCAS feeds its input into, controls the trim tabs on the elevators. This does not change anything about the pilots' inputs to the elevators, but it does change the aerodynamics of the elevators in a way that can limit the pilots' ability to control pitch.
> this plane is more or less stable except that under some conditions it will make the pilot soil their pants at higher AoA, which is where the promises of MCAS come in. Big deal.
If the 737 MAX had been a new aircraft type, it would not have been a problem. There might still have been some adjustment needed to meet FAA certification requirements for stick force (basically, the stick force is supposed to increase with increasing angle of attack, so the pilot has to pull harder to keep the nose going up as you get closer to a stall). But there would not have been a need to cobble together anything like MCAS.
The problem was that Boeing wanted the 737 MAX to be certified under the existing 737 type certificate (because otherwise the potential customers wouldn't want it, since they didn't want to have to re-train and re-certify all their pilots), which meant that the stick force as a function of angle of attack had to be the same as for previous 737s. But the new engines on the 737 MAX made the plane aerodynamically different, so the "natural" stick force was different. MCAS was a software kludge to try to change the stick force.
If the aircraft was a new type this still would have been an issue that would have to be corrected, see FARS 25.173.
But MCAS had enough control authority to override the pilots' inputs; the pilots of both crashed aircraft were desperately trying to pull the nose up, but couldn't because MCAS had put in so much nose down trim that they couldn't counteract it.
> The pilots do have direct control over the stabilizer trim, and have always had the ability to disable the electronic system in case of stabilizer trim runaway. This was not new to the MAX, and would have effectively disabled MCAS.
The ability to disable the automatic stabilizer trim system was not new to the MAX, yes.
What was new to the MAX was that, unlike previous 737s, disabling the automatic stabilizer trim system would also disable the manual electric stabilizer trim system, so that the only way to adjust the trim would be by using the mechanical trim wheel. And it was possible for MCAS to adjust the trim into a range where it was mechanically impossible to adjust it back using the mechanical trim wheel.
It can be. MCAS can be disabled by disabling the electric stability trim system. The problem is that if you do that in a situation where MCAS has already adjusted the trim far enough from where it should be, it can be mechanically impossible to put the trim back where it belongs without using the electric trim system. So you have to first use the electric trim system to put the trim back where it belongs, then disable it so MCAS can't mess it up again.
I get that planes cost more money than I can fathom, and that making a whole fleet of impossible amounts of money costs a gazillion dollars. Still, this one seems spent. Nobody is going to knowingly fly on a 737 Max.
They ought to have retired the plane last year. They can design a new plane (that because of economics, will probably be very similar to this plane), release it when it's been properly vetted, swap out Maxes for it, retrofit those Maxes, etc.
I realize this is naive armchair quarterbacking from someone who has never worked in aviation, but there's a reason that Philip Morris is called Altria now and that Weinstein Co was merged into Spyglass. If the public doesn't trust your brand, no amount of "but we fixed it with this patch we rushed out the door" is going to change that.
This would bankrupt the company.
(Not necessarily uncalled for. But not something it will do on its own.)
> If the public doesn't trust your brand
The public has shown one preference, above all else, when it comes to flying: pricing. The 737 MAX will be renamed, re-certified and nobody but an obsessive minority will avoid flying on it.
(This is why, btw, we need strong airline regulators. Market pressure is ceteris paribus insufficient.)
Is that even possible? From what I understand, it's a strategic company for the United States, so they have to keep it alive no matter what (I recall reading that it's actually a law) - or at least its military branch.
Air travel in the US averages 0.2 deaths per 10 billion passenger-miles.
Driving is 150 deaths per 10B P-M.
Driving across a small town is more likely to kill you than flying across the country.
I also do not agree with the premise that imposing stricter regulation would "double" the cost of tickets. Airline tickets have come down in price for MANY reasons, not just less regulation.
Deregulation happened in 1978. Deaths have been trending down ever since.
I would suggest the site https://www.tylervigen.com/spurious-correlations
The problem here is the regulatory body basically punted and let the company regulate themselves. Like that was going to work...
By 1990 alone inflation adjusted fares had fallen 30% since deregulation. They've fallen more since.
"Airline revenue per passenger mile has declined from an inflation-adjusted 33.3 cents in 1974, to 13 cents in the first half of 2010. In 1974 the cheapest round-trip New York-Los Angeles flight (in inflation-adjusted dollars) that regulators would allow: $1,442. Today one can fly that same route for $268." (https://www.bloomberg.com/businessweek/bwdaily/dnflash/conte...)
This "life and death" talk is just tabloid sensationalism. The numbers don't support it, all. Airline travel is the safest means of transports that exists, or has ever existed, by quite a margin.
Also why I drive to work every day instead of some safer form of transportation.
I strongly disagree with your strong disagree.
Airlines were heavily regulated. We know how it worked.
Nobody is saying regulate them to death. But maybe, just maybe, don't let the company themselves certify their own aircraft when it comes to matters of safety, required training, etc.
I am in disagreement specifically with this absolute quote.
Regulations may or may not be worth the downsides, even when they save lives. The economic costs matter and should be calculated and a reasonable tradeoff should be made.
You can't make a statement like that and then turn around and complain about my hypothetical 300% price increase for a 900% safety increase.
No, pardon me, I meant planes and their maintenance. Airlines setting fares and competing for slots is fine.
Planes and their maintenance are already strictly regulated in the US. Note that the two crashes were not of planes flown by US carriers. The first crash (Lion Air) had maintenance irregularities that contributed to it.
MCAS, however, is not a maintenance failure but a design failure. "More regulation" is not really a good description of what is needed to prevent future design failures like that. What is needed is regulation that can't be outsourced to the companies being regulated, as the FAA was doing.
The regulations worked fine and weren’t super expensive, until the FAA decided to outsource its regulations to the very companies it was supposed to regulate (Boeing).
I will respectfully disagree with you. Most airlines won't tell you your aircraft when you book a ticket and even if they do, they seem allowed to change it at the last minute. If you have spent $500,$1000, $XXXX on a ticket, will you not board if you discover the plane has been switched? Will you avoid airlines that don't guarantee you a certain plane?
There are not many great options to travel long distances quickly. If this plane becomes commonplace, I'm afraid consumers will be forced to use it. If there are other ideas on how this could play out, I'm happy to consider them, but I fear this is nearly a given.
Because the first ticketing site that did that would gain a definite edge. And even if the airline doesn’t tell you what plane is flying, we know what routes and airlines are flying 737 Max’s, which is enough to raise an indicator. If that happens, flying a 737 Max may potentially cause airlines to lose money even if the particular flight isn’t a 737 Max, because it might be one.
Its standard ICAO terminology.
I haven't seen that sorta thing on booking sites, but its common on sites like FlightAware.
https://i.imgur.com/h8k2IFK.jpg
https://i.imgur.com/7xfQpQX.jpg
https://i.imgur.com/7Ax2AQh.jpg
I don't think this is remotely true. I just checked Delta and British Airways; both show the aircraft type in "details". (Pick the 747 flights from BA while you still can!)
> even if they do, they seem allowed to change it at the last minute
Airlines shuffle aircraft occasionally, but usually the aircraft type for a particular flight is predictable. If airline A flies the 737 Max and airline B flies the A320 on the same route, people will flock to airline B.
[1] https://en.wikipedia.org/wiki/List_of_Boeing_737_MAX_orders_...
I assure you that outside of people interested in tech, few I know have any idea what the MAX8 is, how to tell one from the NG or an A320. Once the plane flies it’s going to be business as usual.
Most people are not well represented by the fine folks on HN.
This is all about operator logistics and lock-in by costs of retraining and infrastructure. (I guess, this may be the real point to be addressed, since, as this is such a crucial factor, procedures are prone to be repeated in other configurations in the future. Failures are highly likely to be repeated, regardless of the actor.)
Edit: To emphasize the last thought, the 737 Max may be more of a systemic failure of the entire business, its regulations and how they are conducted, than a failure by a single actor on a single instance.
After a few years, no one will care anymore.
- buggy
- the one where bugs were not yet found
I only remember hearing about "mathematically proven software" as an undergrad and just googled to find this name. I've always been interested in learning more of what it's about but never jumped in.
How Amazon Web Services Uses Formal Methods
Formal verification is a good and useful tool, but it provably cannot cover the entire system, and practical limitations will limit it even further.
Formal verification of source code is still subject to compiler bugs. Formally proven compilers are subject to bugs in the larger system (IIRC Csmith was able to find an incorrectness in code generated by CompCert because of a bug in a system header file).
If the hardware is behaving in spec (e.g. 1 out of 3 computers fails) and you properly formally verified the software to that spec, the software will not behave badly.
I would imagine the MCAS belongs to this class. But even if your software is correct, the design it implements might be flawed, say by assuming the input you get from a single fallible sensor is to be trusted.