[SystemSafety] Correctness by Construction

[Dewi Daniels]

I agree with Tom.

You're looking at this as a software problem. I don't think you'd find the
problem by doing more software testing. The software developers were told
to apply a certain amount of nose down trim when the angle of attack
exceeded some limit and that was what the software did. This was a systems
problem.

As I wrote in my SSS''20 paper, I believe that Boeing made two main
mistakes:

1. They assessed MCAS as DAL C because it was intended to have limited
authority (initially 0.6 degrees, later increased to 2.5 degrees). They
failed to realise that in the event of a failure, MCAS would have unlimited
authority and could apply full nose down trim. Once they convinced
themselves and the FAA that MCAS was DAL C, there would have been much less
FAA oversight after that point.
.
2. My understanding is that the only validation carried out of the
requirement was that they applied 2.5 degrees of nose down trim in the
simulator and confirmed the pilot was able to counteract the nose down trim
by using the yoke and electric trim. It doesn't appear they simulated an
AoA sensor failure either during simulation or during flight test. Had they
done so, they would have realised that if the AoA sensor failed hard-over,
applying nose down trim would not reduce the reported angle of attack, so
MCAS would apply nose down trim repeatedly until full nose down trim was
applied.

As I said at the end of my SSS'20 keynote, I believe that to improve
aircraft safety, we need to get better at writing requirements and
validating requirements. I think that formal methods have a role to play in
getting the requirements right as well as in demonstrating that the
software implements the requirements correctly.  There have been no
hull-loss accidents in passenger service caused by the software
implementing the requirements incorrectly, but there have been several
fatal accidents where the software implemented its requirements correctly,
but the requirements specified unsafe behaviour under some unforeseen
circumstance. These include the A320 that overran the runway in Warsaw in
1993 as well as the Boeing 737 MAX accidents.

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 11:45, Tom Ferrell <tom at faaconsulting.com> 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 <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
>
>
>
> _______________________________________________
>
> The System Safety Mailing List
>
> 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/2d816298/attachment.html>