4 ms·

This was already submitted and discussed at https://news.ycombinator.com/item?id=14336897 https://news.ycombinator.com/item?id=14336897 and https://news.ycombin

This was already submitted and discussed at https://news.ycombinator.com/item?id=14336897 https://news.ycombinator.com/item?id=14336897 and https://news.ycombinator.com/item?id=14328294 https://news.ycombinator.com/item?id=14328294. My summary at https://news.ycombinator.com/item?id=14329082 https://news.ycombinator.com/item?id=14329082 is still the most in depth researched as far as I can tell (I actually read a lot of the air safety bureau report). Basically Northrup Grumman's ADIRU units had sporadic software bugs (off by one - typical of software written in needlessly low level languages) and the Airbus control system that combined the output of the three redundant ADIRUs didn't properly deal with the case of failure in one of the three (even if 2/3 agreed with GPS!), didn't provide transparent training and resolution procedures to pilots for this class of situation, and was generally trusting the broken unit instead of the other two or the GPS which were operating fine. Even calling the crisis center of the major airline for assistance on the ground couldn't help resolve the situation. So... problems in both companies, but Airbus is mostly to blame, even if testing could not be expected to tease out all bugs in third party components, primarily because they were not logging issues and resolving them from the millions of flight hours these things already had, and because they had not tested their fly-by-wire system with worst case input, ie. what's the point of redundancy if you trust the broken unit?

perilunar 9y ago
Also https://news.ycombinator.com/item?id=14330913 https://news.ycombinator.com/item?id=14330913
mathgenius 9y ago
After the Intel FDIV bug [1] they started using formal verification to make sure the cpu's did what they said they would. I don't understand why they don't do the same for these avionic systems. Maybe it's just not worth it to the company. [1] https://en.wikipedia.org/wiki/Pentium_FDIV_bug https://en.wikipedia.org/wiki/Pentium_FDIV_bug
- flashmob 9y ago
  Would you say that this has limitations and it's not a silver bullet? Eg. What if your software added numbers, formal verification proved that your program was indeed correct because it added the numbers. However, it missed the requirement that you also had to do subtraction, which for some reason was omitted in the specification.
  - mannykannot 9y ago
    You would be no worse off in this situation. Writing a formal spec. arguably makes it harder to overlook such issues. Formal verification is good at catching things like off-by-one errors, where the problem is not in the spec.
  - mathgenius 9y ago
    Yes, I agree of course. Garbage-in-garbage-out has many manifestations.
mannykannot 9y ago
Leaky abstractions... nominally, this appears to be a triply-redundant system, but due to the way the systems interacted, a single faulty unit apparently overrode two units that were working correctly (or were at least responding safely to the situation.) I have not finished reading the report, and I am interested to know if it contained anything to address this apparent systems-engineering level issue, such as how likely it is that there are other potential breakdowns of redundancy. I am not sure whether there is much that can be done in the way of pilot training and resolution procedures for this class of problem. Trying to figure out if a subsystem is faulty, and if so, which one, when they are interconnected by complex and frequently opaque rules, is not easy. I do not think that more information would help, given that the crew was already getting more diagnostic messages than they could handle in real time.

perilunar 9y ago

Also https://news.ycombinator.com/item?id=14330913 https://news.ycombinator.com/item?id=14330913

mathgenius 9y ago

After the Intel FDIV bug [1] they started using formal verification to make sure the cpu's did what they said they would. I don't understand why they don't do the same for these avionic systems. Maybe it's just not worth it to the company. [1] https://en.wikipedia.org/wiki/Pentium_FDIV_bug https://en.wikipedia.org/wiki/Pentium_FDIV_bug

flashmob 9y ago
Would you say that this has limitations and it's not a silver bullet? Eg. What if your software added numbers, formal verification proved that your program was indeed correct because it added the numbers. However, it missed the requirement that you also had to do subtraction, which for some reason was omitted in the specification.
- mannykannot 9y ago
  You would be no worse off in this situation. Writing a formal spec. arguably makes it harder to overlook such issues. Formal verification is good at catching things like off-by-one errors, where the problem is not in the spec.
- mathgenius 9y ago
  Yes, I agree of course. Garbage-in-garbage-out has many manifestations.

mannykannot 9y ago

Leaky abstractions... nominally, this appears to be a triply-redundant system, but due to the way the systems interacted, a single faulty unit apparently overrode two units that were working correctly (or were at least responding safely to the situation.) I have not finished reading the report, and I am interested to know if it contained anything to address this apparent systems-engineering level issue, such as how likely it is that there are other potential breakdowns of redundancy. I am not sure whether there is much that can be done in the way of pilot training and resolution procedures for this class of problem. Trying to figure out if a subsystem is faulty, and if so, which one, when they are interconnected by complex and frequently opaque rules, is not easy. I do not think that more information would help, given that the crew was already getting more diagnostic messages than they could handle in real time.