[SystemSafety] Correctness by Construction

[Olwen Morgan]

On 10/07/2020 11:24, Dewi Daniels wrote:

<snip>
>
>  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.
>
<snip>


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.


Olwen






> Yours,
>
> Dewi Daniels | Director | Software Safety Limited
>
> Telephone +44 7968 837742 | Email d 
> <mailto:ddaniels at verocel.com>ewi.daniels at software-safety.com 
> <mailto:ewi.daniels at software-safety.com>
>
> Software Safety Limited is a company registered in England and Wales. 
> Company number: 9390590. Registered office: Fairfield, 30F Bratton 
> Road, West Ashton, Trowbridge, United Kingdom BA14 6AZ
>
>
>
> On Fri, 10 Jul 2020 at 10:42, Michael Jackson <jacksonma at acm.org 
> <mailto:jacksonma at acm.org>> wrote:
>
>     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?
>
>     -- Michael Jackson
>
>
>     _______________________________________________
>     The System Safety Mailing List
>     systemsafety at TechFak.Uni-Bielefeld.DE
>     <mailto:systemsafety at TechFak.Uni-Bielefeld.DE>
>     Manage your subscription:
>     https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200710/4c17e2df/attachment-0001.html>