[SystemSafety] Correctness by Construction

[Olwen Morgan]

Well-designed stress tests could have simulated a faulty AoA sensor.


Olwen


On 10/07/2020 11:45, Tom Ferrell wrote:
>
> On 10/07/2020 11:24, Olwen Morgan wrote:
>
> <snip>
>
> With MCAS, iterated tests or stress tests of the software might have 
> revealed the problem.
>
> <snip>
>
> 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.
>
> *From:* systemsafety 
> <systemsafety-bounces at lists.techfak.uni-bielefeld.de> *On Behalf Of 
> *Olwen Morgan
> *Sent:* Friday, July 10, 2020 6:34 AM
> *To:* systemsafety at lists.techfak.uni-bielefeld.de
> *Subject:* Re: [SystemSafety] Correctness by Construction
>
> 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  <mailto: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/e9fce7a3/attachment.html>