[SystemSafety] Correctness by Construction

[Dewi Daniels]

Michael,

I presented a keynote on the Boeing 737 MAX accidents at SSS'20.

https://scsc.uk/e619prog

There is no evidence that the MCAS software failed to satisfy its
requirements. It appears that the MCAS software behaved correctly according
to its requirements, but that those requirements specified unsafe
behaviour. It seems that the system safety engineers and the 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.

Yours,

Dewi Daniels | Director | Software Safety Limited

Telephone +44 7968 837742 | Email d <ddaniels at verocel.com>
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> 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
> 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/17d40d3b/attachment.html>