<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<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:"Angsana New";
        panose-1:2 2 6 3 5 4 5 2 3 4;}
@font-face
        {font-family:"Cordia New";
        panose-1:2 11 3 4 2 2 2 2 2 4;}
@font-face
        {font-family:"Cambria Math";
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:DengXian;
        panose-1:2 1 6 0 3 1 1 1 1 1;}
@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;}
@font-face
        {font-family:"\@DengXian";
        panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        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;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
pre
        {mso-style-priority:99;
        mso-style-link:"HTML Vorformatiert Zchn";
        margin:0cm;
        margin-bottom:.0001pt;
        font-size:10.0pt;
        font-family:"Courier New";}
p.msonormal0, li.msonormal0, div.msonormal0
        {mso-style-name:msonormal;
        mso-margin-top-alt:auto;
        margin-right:0cm;
        mso-margin-bottom-alt:auto;
        margin-left:0cm;
        font-size:11.0pt;
        font-family:"Calibri",sans-serif;}
span.HTMLVorformatiertZchn
        {mso-style-name:"HTML Vorformatiert Zchn";
        mso-style-priority:99;
        mso-style-link:"HTML Vorformatiert";
        font-family:Consolas;}
p.HTMLPreformatted, li.HTMLPreformatted, div.HTMLPreformatted
        {mso-style-name:"HTML Preformatted";
        mso-style-link:"HTML Preformatted Char";
        margin:0cm;
        margin-bottom:.0001pt;
        font-size:11.0pt;
        font-family:"Calibri",sans-serif;}
span.HTMLPreformattedChar
        {mso-style-name:"HTML Preformatted Char";
        mso-style-priority:99;
        mso-style-link:"HTML Preformatted";
        font-family:Consolas;}
span.E-MailFormatvorlage23
        {mso-style-type:personal;
        font-family:"Calibri",sans-serif;
        color:windowtext;}
span.E-MailFormatvorlage24
        {mso-style-type:personal;
        font-family:"Arial",sans-serif;
        color:#1F497D;
        font-weight:normal;
        font-style:normal;}
span.E-MailFormatvorlage26
        {mso-style-type:personal-compose;
        font-family:"Arial",sans-serif;
        color:windowtext;
        font-weight:normal;
        font-style:normal;}
.MsoChpDefault
        {mso-style-type:export-only;
        font-size:10.0pt;}
@page WordSection1
        {size:612.0pt 792.0pt;
        margin:72.0pt 72.0pt 72.0pt 72.0pt;}
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]-->
</head>
<body lang="DE" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black">Hi Olwen,<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black">they did simulations already in November 2016 but outcome by experienced pilots “awful behavior of the software” was not recognized in the management.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black">Hiding of problems in the management counts for me more than technical route causes here.<o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black">Ref, sorry only in german:<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:#1F497D"><a href="https://www.sueddeutsche.de/wirtschaft/boeing-737-max-absturz-ursache-untersuchung-1.4647909"><span lang="EN-US">https://www.sueddeutsche.de/wirtschaft/boeing-737-max-absturz-ursache-untersuchung-1.4647909</span></a></span><span lang="EN-US" style="font-size:10.0pt;font-family:"Arial",sans-serif;color:#1F497D"><o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.0pt;font-family:"Arial",sans-serif;color:#1F497D"><o:p> </o:p></span></p>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">Best regards<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-bottom:12.0pt"><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">Dietmar</span><span lang="EN-US" style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1F497D"> </span><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">KINALZYK</span><span lang="EN-US" style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1F497D"><br>
</span><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">Principal Development Engineer</span><span lang="EN-US" style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1F497D"><br>
</span><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">Product Safety & NON-PT Safety</span><span lang="EN-US" style="font-size:14.0pt;font-family:"Arial",sans-serif;color:black"><br>
AVL Software and Functions GmbH<br>
</span><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">Im Gewerbepark B29</span><span lang="EN-US" style="font-size:14.0pt;font-family:"Arial",sans-serif;color:black">,
</span><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">93059</span><span lang="EN-US" style="font-size:14.0pt;font-family:"Arial",sans-serif;color:black"> </span><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">Regensburg</span><span lang="EN-US" style="font-size:14.0pt;font-family:"Arial",sans-serif;color:black"><br>
</span><span lang="EN-US" style="font-family:"Arial",sans-serif;color:black">Germany</span><span lang="EN-US" style="font-size:14.0pt;font-family:"Arial",sans-serif;color:black"><br>
</span><u><span style="font-family:"Arial",sans-serif;color:black"><a href="www.avl-functions.com"><span lang="EN-US" style="color:black">www.avl-functions.com</span></a></span></u><span lang="EN-US" style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1F497D"><br>
<br>
</span><span lang="EN-US"><o:p></o:p></span></p>
</div>
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b>Von:</b> systemsafety <systemsafety-bounces@lists.techfak.uni-bielefeld.de>
<b>Im Auftrag von </b>Olwen Morgan<br>
<b>Gesendet:</b> Freitag, 10. Juli 2020 14:55<br>
<b>An:</b> Tom Ferrell <tom@faaconsulting.com>; systemsafety@lists.techfak.uni-bielefeld.de<br>
<b>Betreff:</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>
<p>Well-designed stress tests could have simulated a faulty AoA sensor.<o:p></o:p></p>
<p><o:p> </o:p></p>
<p>Olwen<o:p></o:p></p>
<p><o:p> </o:p></p>
<div>
<p class="MsoNormal">On 10/07/2020 11:45, Tom Ferrell wrote:<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<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 0cm 0cm 0cm">
<p class="MsoNormal"><b>From:</b> systemsafety <a 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 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:105%"> 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"><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 lang="FR" style="font-size:10.0pt;font-family:"Arial",sans-serif">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><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">jacksonma@acm.org</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-top:5.0pt;margin-right:0cm;margin-bottom:5.0pt">
<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://urldefense.com/v3/__https:/lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety__;!!Oq50-tQ!5mEv8mFepFmJDme35SE9uO3fZcR1LEFQL2gc06NuxnGd_yi3R-rDjHrSE4attYfeZEVU$" target="_blank">
https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><o:p></o:p></p>
</blockquote>
</div>
<p class="MsoNormal"><br>
<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">systemsafety@TechFak.Uni-Bielefeld.DE</a><o:p></o:p></pre>
<pre>Manage your subscription: <a href="https://urldefense.com/v3/__https:/lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety__;!!Oq50-tQ!5mEv8mFepFmJDme35SE9uO3fZcR1LEFQL2gc06NuxnGd_yi3R-rDjHrSE4attYfeZEVU$">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><o:p></o:p></pre>
</blockquote>
</blockquote>
</div>
</body>
</html>