<div dir="ltr"><div>I agree with Tom.</div><div><br></div><div>You're looking at this as a software problem. I don't think you'd find the problem by doing more software testing. The software developers were told to apply a certain amount of nose down trim when the angle of attack exceeded some limit and that was what the software did. This was a systems problem.</div><div><br></div><div>As I wrote in my SSS''20 paper, I believe that Boeing made two main mistakes:</div><div><br></div><div>1. They assessed MCAS as DAL C because it was intended to have limited authority (initially 0.6 degrees, later increased to 2.5 degrees). They failed to realise that in the event of a failure, MCAS would have unlimited authority and could apply full nose down trim. Once they convinced themselves and the FAA that MCAS was DAL C, there would have been much less FAA oversight after that point.<br></div><div>.</div><div>2. My understanding is that the only validation carried out of the requirement was that they applied 2.5 degrees of nose down trim in the simulator and confirmed the pilot was able to counteract the nose down trim by using the yoke and electric trim. It doesn't appear they simulated an AoA sensor failure either during simulation or during flight test. Had they done so, they would have realised that if the AoA sensor failed hard-over, applying nose down trim would not reduce the reported angle of attack, so MCAS would apply nose down trim repeatedly until full nose down trim was applied.</div><div><br></div><div>As I said at the end of my SSS'20 keynote, I believe that to improve aircraft safety, we need to get better at writing requirements and validating requirements. I think that formal methods have a role to play in getting the requirements right as well as in demonstrating that the software implements the requirements correctly. There have been no hull-loss accidents in passenger service caused by the software implementing the requirements incorrectly, but there have been several fatal accidents where the software implemented its requirements correctly, but the requirements specified unsafe behaviour under some unforeseen circumstance. These include the A320 that overran the runway in Warsaw in 1993 as well as the Boeing 737 MAX accidents.<br></div><div><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><p><a name="SignatureSanitizer_SafeHtmlFilter_UNIQUE_ID_SafeHtmlFilter__MailAutoSig"><span style="font-size:10pt;font-family:Arial,sans-serif">Yours,</span></a></p><p><span style="font-family:Arial,sans-serif;font-size:10pt">Dewi Daniels | Director | Software Safety Limited</span><br></p><p><span style="font-size:10pt;font-family:Arial,sans-serif" lang="FR">Telephone +44 7968 837742 | Email </span><span style="font-size:10pt;font-family:Arial,sans-serif;color:purple" lang="FR"><a href="mailto:ddaniels@verocel.com" target="_blank">d</a><a href="mailto:ewi.daniels@software-safety.com" target="_blank">ewi.daniels@software-safety.com</a></span></p><p><font face="Arial, sans-serif">Software Safety Limited is a company registered in England and Wales. Company number: </font><font face="Arial, sans-serif">9390590</font><font face="Arial, sans-serif">. Registered office: Fairfield, 30F Bratton Road, West Ashton, Trowbridge</font><span style="font-size:small;font-family:Arial,sans-serif">, United Kingdom </span><span style="font-size:small;font-family:Arial,sans-serif">BA14 6AZ</span></p></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 10 Jul 2020 at 11:45, Tom Ferrell <<a href="mailto:tom@faaconsulting.com">tom@faaconsulting.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div lang="EN-US">
<div class="gmail-m_8165972440981141968WordSection1">
<p class="MsoNormal">On 10/07/2020 11:24, Olwen Morgan wrote:<u></u><u></u></p>
<p><snip><u></u><u></u></p>
<p class="MsoNormal">With MCAS, iterated tests or stress tests of the software might have revealed the problem.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><snip><u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">I would suggest you are still looking at this as a software problem. The MCAS behavior that led to the crashes also involved a single threaded and malfunctioning Angle of Attack (AoA) sensor. There was also involvement of the pilot in
resetting the MCAS which allowed it to make multiple unbounded control inputs. While this could have all been simulated to test the software in isolation as suggested, it is unlikely in my view that this would have surfaced what was a complex behavioral problem
at the aircraft level. <u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div style="border-color:rgb(225,225,225) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0in 0in">
<p class="MsoNormal"><b>From:</b> systemsafety <<a href="mailto:systemsafety-bounces@lists.techfak.uni-bielefeld.de" target="_blank">systemsafety-bounces@lists.techfak.uni-bielefeld.de</a>>
<b>On Behalf Of </b>Olwen Morgan<br>
<b>Sent:</b> Friday, July 10, 2020 6:34 AM<br>
<b>To:</b> <a href="mailto:systemsafety@lists.techfak.uni-bielefeld.de" target="_blank">systemsafety@lists.techfak.uni-bielefeld.de</a><br>
<b>Subject:</b> Re: [SystemSafety] Correctness by Construction<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<p><u></u> <u></u></p>
<div>
<p class="MsoNormal">On 10/07/2020 11:24, Dewi Daniels wrote:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal"><snip><u></u><u></u></p>
</div>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal" style="margin-bottom:8pt;line-height:106%"> requirements engineers only considered a single activation of MCAS. They do not appear to have considered the possibility that MCAS could activate repeatedly, eventually driving the stabilizer
to a fully nose down position.<u></u><u></u></p>
</div>
</blockquote>
<p><snip><u></u><u></u></p>
<p><u></u> <u></u></p>
<p>This goes nicely with my example of the Wichman-Hill PRANG. The essence of the required behaviour is a condition on repeated calls to the routine that generates a single random number. Only iterative testing could provide confidence in its correctness. With
MCAS, iterated tests or stress tests of the software might have revealed the problem.<u></u><u></u></p>
<p><u></u> <u></u></p>
<p>Olwen<u></u><u></u></p>
<p><u></u> <u></u></p>
<p><u></u> <u></u></p>
<p><u></u> <u></u></p>
<p><u></u> <u></u></p>
<p><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<div>
<div>
<div>
<div>
<p><a name="m_8165972440981141968_SignatureSanitizer_SafeHtmlFilter_UNIQUE"><span style="font-size:10pt;font-family:"Arial",sans-serif">Yours,</span></a><u></u><u></u></p>
<p><span style="font-size:10pt;font-family:"Arial",sans-serif">Dewi Daniels | Director | Software Safety Limited</span><u></u><u></u></p>
<p><span style="font-size:10pt;font-family:"Arial",sans-serif" lang="FR">Telephone +44 7968 837742 | Email <span style="color:purple"><a href="mailto:ddaniels@verocel.com" target="_blank">d</a><a href="mailto:ewi.daniels@software-safety.com" target="_blank">ewi.daniels@software-safety.com</a></span></span><u></u><u></u></p>
<p><span style="font-family:"Arial",sans-serif">Software Safety Limited is a company registered in England and Wales. Company number: 9390590. Registered office: Fairfield, 30F Bratton Road, West Ashton, Trowbridge</span><span style="font-size:12pt;font-family:"Arial",sans-serif">,
United Kingdom BA14 6AZ</span><u></u><u></u></p>
</div>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Fri, 10 Jul 2020 at 10:42, Michael Jackson <<a href="mailto:jacksonma@acm.org" target="_blank">jacksonma@acm.org</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0in 0in 0in 6pt;margin-left:4.8pt;margin-right:0in">
<p class="MsoNormal">CbyC is invaluable in avoiding errors in reasoning about formal models. But the relationship of a formal model---whether of a computer or of the real world of a cyber-physical system---may be a more prolific source of faiure. Recent posts
cited the 737Max8 disasters. Were these due to formal errors in MCAS code? <br>
<br>
-- Michael Jackson<br>
<br>
<br>
_______________________________________________<br>
The System Safety Mailing List<br>
<a href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE" target="_blank">systemsafety@TechFak.Uni-Bielefeld.DE</a><br>
Manage your subscription: <a href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety" target="_blank">
https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><u></u><u></u></p>
</blockquote>
</div>
<p class="MsoNormal"><br>
<br>
<u></u><u></u></p>
<pre>_______________________________________________<u></u><u></u></pre>
<pre>The System Safety Mailing List<u></u><u></u></pre>
<pre><a href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE" target="_blank">systemsafety@TechFak.Uni-Bielefeld.DE</a><u></u><u></u></pre>
<pre>Manage your subscription: <a href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety" target="_blank">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><u></u><u></u></pre>
</blockquote>
</div>
</div>
_______________________________________________<br>
The System Safety Mailing List<br>
<a href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE" target="_blank">systemsafety@TechFak.Uni-Bielefeld.DE</a><br>
Manage your subscription: <a href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety" rel="noreferrer" target="_blank">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></blockquote></div>