Thoughts and clarifications

Posted Sep 23, 2024 9:26 UTC (Mon) by Wol (subscriber, #4433)
In reply to: Thoughts and clarifications by farnz
Parent article: Whither the Apple AGX graphics driver?

While it may not be what Knuth was thinking of, I also think of it as pointing out that a formal proof merely proves that the mathematical model is internally consistent.

It does not prove that what the model does is what reality does! In a properly specified system, maths and science(reality) usually agree, but there's no guarantee ...

Cheers,
Wol

Thoughts and clarifications

Posted Sep 23, 2024 11:56 UTC (Mon) by pizza (subscriber, #46) [Link] (5 responses)

> It does not prove that what the model does is what reality does! In a properly specified system, maths and science(reality) usually agree, but there's no guarantee ...

This has been my experience.

...The software running on the 737MAX's MCAS was "provably correct" .. for its specifications.

(It turns out that the words "properly specified" are about as common as unicorn-riding sasquatches...)

Thoughts and clarifications

Posted Sep 23, 2024 12:01 UTC (Mon) by farnz (subscriber, #17727) [Link] (4 responses)

Reference for "the software running on the 737MAX's MCAS was "provably correct""? I can't find any evidence anywhere that the MCAS was formally verified at all - merely that it was tested correct, and Boeing asserted to the FAA that the testing covered all plausible scenarios.

Thoughts and clarifications

Posted Sep 23, 2024 14:06 UTC (Mon) by pizza (subscriber, #46) [Link] (3 responses)

> Reference for "the software running on the 737MAX's MCAS was "provably correct""?

I'm giving Boeing's software folks the benefit of the doubt, because the MCAS debacle was a failure of specification (on multiple levels), not one of implementation.

After all, one can't test/validate compliance with a requirement that doesn't exist.

> Boeing asserted to the FAA that the testing covered all plausible scenarios.

It did! Unfortunately, many of those "plausible scenarios" required pilots to be trained differently [1], but a different part of Boeing explicitly said that wasn't necessary [2].

[1] ie recognize what was going on, and flip a circuit breaker (!) to disable MCAS
[2] One of the main selling points of the MAX

737 MAX only tested, not proven correct

Posted Sep 23, 2024 14:40 UTC (Mon) by farnz (subscriber, #17727) [Link] (2 responses)

There is a requirement underpinning all avionics that the aircraft's behaviour is safe in the event of a data source failing, and that the avionics are able to detect that a data source has become unreliable and enter the failsafe behaviour mode. This is a specification item for MCAS, and Boeing asserted to the FAA that they had tested MCAS and confirmed that, in the event of an AoA sensor fault, MCAS would detect the fault and enter the failsafe behaviours.

Boeing's tests for this, however, were grossly inadequate, and at least 3 different failure conditions have been found which were not covered by the tests: first is that "AoA DISAGREE" was an optional indication, available during the tests, but not in production MCAS unless purchased (20% of the fleet). Second is that they did not test enough bit error cases, and later investigation found a 5 bit error case that was catastrophic. And third was that the procedure for handling MCAS issues assumed that the pilot would have time to follow the checklist; in practice, the training issues meant that pilots didn't even realise there was a checklist.

737 MAX only tested, not proven correct

Posted Sep 23, 2024 15:49 UTC (Mon) by pizza (subscriber, #46) [Link] (1 responses)

> first is that "AoA DISAGREE" was an optional indication,

It's worse than that -- _redundant sensors_ were optional.

..and they were optional because one set of folks had a different set of functional specifications than another, and management was disincentivized to notice.

737 MAX only tested, not proven correct

Posted Sep 23, 2024 16:23 UTC (Mon) by paulj (subscriber, #341) [Link]

Went and had a read, as it seems you and farnz don't quite agree and/or are talking about slightly different things. ICBW, but my read of the FAA summary report is:

FAA "Safety Item #1: USE OF SINGLE ANGLE OF ATTACK (AOA) SENSOR" - this refers to the use of /data/ from a single AoA sensor by MCAS.

FAA "Safety item #5: AOA DISAGREE:" - refers to the "AOA DISAGREE" warning in the cockpit FDU, which somehow was tied to the optional "AoA Indicator gauge" feature for the FDU, which airlines had to purchases.

AFAICT from the FAA summary. I.e., the change was entirely in the logic - because there was no action item to retro-fit another AoA vane to the 737 Max. Excluding training and maintenance requirements, aircraft changes were all logic update to do better filtering of the 2 AoA signals, with better differential error detection, and cease ploughing ahead with MCAS commands based on measurements from just 1 vane - which could be faulty. Other aircraft safety items added limits, damping and margins, to prevent runaway MCAS crashing aircraft.

Stunning issues really.