<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<div class="moz-cite-prefix">On 10/07/2020 11:24, Dewi Daniels
wrote:</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix"><snip><br>
</div>
<blockquote type="cite"
cite="mid:CANQd8eV267FDwdov42=PPB+TLAbqeN+Dv6Mq5KsGjfhXuwGK0w@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr"><br>
<p class="MsoNormal" style="margin:0cm 0cm
8pt;line-height:107%;font-size:11pt;font-family:"Calibri",sans-serif"> 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.</p>
</div>
</blockquote>
<p><snip></p>
<p><br>
</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.</p>
<p><br>
</p>
<p>Olwen</p>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:CANQd8eV267FDwdov42=PPB+TLAbqeN+Dv6Mq5KsGjfhXuwGK0w@mail.gmail.com">
<div dir="ltr">
<p class="MsoNormal" style="margin:0cm 0cm
8pt;line-height:107%;font-size:11pt;font-family:"Calibri",sans-serif"><span></span></p>
<div>
<div>
<div dir="ltr" class="gmail_signature"
data-smartmail="gmail_signature">
<div dir="ltr">
<p><a
name="SignatureSanitizer_SafeHtmlFilter_UNIQUE_ID_SafeHtmlFilter__MailAutoSig"
moz-do-not-send="true"><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" 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></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 10:42,
Michael Jackson <<a href="mailto:jacksonma@acm.org"
moz-do-not-send="true">jacksonma@acm.org</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">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"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
The System Safety Mailing List
<a class="moz-txt-link-abbreviated" href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE">systemsafety@TechFak.Uni-Bielefeld.DE</a>
Manage your subscription: <a class="moz-txt-link-freetext" href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></pre>
</blockquote>
</body>
</html>