<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<p>Well-designed stress tests could have simulated a faulty AoA
sensor.</p>
<p><br>
</p>
<p>Olwen</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 10/07/2020 11:45, Tom Ferrell wrote:<br>
</div>
<blockquote type="cite"
cite="mid:MN2PR13MB26056CA3FA6AE4D2C6CE681AB9650@MN2PR13MB2605.namprd13.prod.outlook.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="Generator" content="Microsoft Word 15 (filtered
medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0in;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:Consolas;}
span.EmailStyle21
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
<div class="WordSection1">
<p class="MsoNormal">On 10/07/2020 11:24, Olwen Morgan wrote:<o:p></o:p></p>
<p><snip><o:p></o:p></p>
<p class="MsoNormal">With MCAS, iterated tests or stress tests
of the software might have revealed the problem.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><snip><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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. <o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div style="border:none;border-top:solid #E1E1E1
1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal"><b>From:</b> systemsafety
<a class="moz-txt-link-rfc2396E" href="mailto:systemsafety-bounces@lists.techfak.uni-bielefeld.de"><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 class="moz-txt-link-abbreviated" href="mailto:systemsafety@lists.techfak.uni-bielefeld.de">systemsafety@lists.techfak.uni-bielefeld.de</a><br>
<b>Subject:</b> Re: [SystemSafety] Correctness by
Construction<o:p></o:p></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p><o:p> </o:p></p>
<div>
<p class="MsoNormal">On 10/07/2020 11:24, Dewi Daniels wrote:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><snip><o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"
style="margin-bottom:8.0pt;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.<o:p></o:p></p>
</div>
</blockquote>
<p><snip><o:p></o:p></p>
<p><o:p> </o:p></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.<o:p></o:p></p>
<p><o:p> </o:p></p>
<p>Olwen<o:p></o:p></p>
<p><o:p> </o:p></p>
<p><o:p> </o:p></p>
<p><o:p> </o:p></p>
<p><o:p> </o:p></p>
<p><o:p> </o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<div>
<p><a
name="SignatureSanitizer_SafeHtmlFilter_UNIQUE"
moz-do-not-send="true"><span
style="font-size:10.0pt;font-family:"Arial",sans-serif">Yours,</span></a><o:p></o:p></p>
<p><span
style="font-size:10.0pt;font-family:"Arial",sans-serif">Dewi
Daniels | Director | Software Safety Limited</span><o:p></o:p></p>
<p><span
style="font-size:10.0pt;font-family:"Arial",sans-serif"
lang="FR">Telephone +44 7968 837742 | Email <span
style="color:purple"><a
href="mailto:ddaniels@verocel.com"
target="_blank" moz-do-not-send="true">d</a><a
href="mailto:ewi.daniels@software-safety.com" target="_blank"
moz-do-not-send="true">ewi.daniels@software-safety.com</a></span></span><o:p></o:p></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:12.0pt;font-family:"Arial",sans-serif">,
United Kingdom BA14 6AZ</span><o:p></o:p></p>
</div>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Fri, 10 Jul 2020 at 10:42, Michael
Jackson <<a href="mailto:jacksonma@acm.org"
moz-do-not-send="true">jacksonma@acm.org</a>>
wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC
1.0pt;padding:0in 0in 0in
6.0pt;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" moz-do-not-send="true">systemsafety@TechFak.Uni-Bielefeld.DE</a><br>
Manage your subscription: <a
href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety"
target="_blank" moz-do-not-send="true">
https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><o:p></o:p></p>
</blockquote>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<pre>_______________________________________________<o:p></o:p></pre>
<pre>The System Safety Mailing List<o:p></o:p></pre>
<pre><a href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE" moz-do-not-send="true">systemsafety@TechFak.Uni-Bielefeld.DE</a><o:p></o:p></pre>
<pre>Manage your subscription: <a href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety" moz-do-not-send="true">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><o:p></o:p></pre>
</blockquote>
</div>
</blockquote>
</body>
</html>