[SystemSafety] Correctness by Construction

[Dewi Daniels]

Michael,

At Altran, they use Z to express requirements. I believe that Altran are
moving to Alloy. At Callen-Lenz, we're using D-RisQ's Kapture requirements
language.

You make a good point about the physical problem world. Your observation
highlights the boundaries of Correctness by Construction. Consider a flight
control system. Just because we can prove that the code is a correct
implementation of a PID controller (for example) doesn't mean that the
flight control system flies the aircraft accurately (or at all). That
depends on how the PID controller is tuned and how it interacts with the
airframe. We can verify the flight control system using a flight model,
though the flight model itself is an abstraction of the real aircraft. Even
if we can show that the flight control system flies the aircraft
accurately, it doesn't necessarily mean that the aircraft has desirable
handling qualities.

This doesn't mean that Correctness by Construction has no value. At
Callen-Lenz, we're developing a flight control system for air taxis and
personal air vehicles. We're using formal methods (specifically D-RisQ's
Modelworks, CLawZ and FEVER tools) to verify that the binary is a correct
implementation of the software requirements, which are expressed in
Kapture. That greatly reduces the number of tests that we need to write (it
does not eliminate testing altogether), meaning that we can deploy working,
certifiable code very quickly using our model-based development environment.

One of the best compliments I've received was when someone said, "Dewi has
the ability to just write working code". I'm not sure that person
appreciated how much thought I'd put into the requirements and the design
before I wrote a single line of code.

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 Tue, 14 Jul 2020 at 10:14, Michael Jackson <jacksonma at acm.org> wrote:

> Dewi:
>
> Yes: but how are requirements to be expressed and communicated to the
> software developers? And if the requirements are communicated, how are the
> software developers to reason reliably about the physical problem world
> where the important requirements are located and defined, and will---or
> will not---be satisfied? And is 'correctness' a proper word to use about
> artifacts in the physical world at the scales relevant to software
> engineering?
>
> Yours,
>
> -- Michael
>
> > On 13 Jul 2020, at 20:55, Dewi Daniels <dewi.daniels at software-safety.com>
> wrote:
> >
> > Michael,
> >
> > In the context of “Correctness by Construction”, I would say that
> Correctness means “compliance with requirements”.
> >
> > Yours,
> > Dewi
> >
> > On Mon, 13 Jul 2020 at 13:59, Michael Jackson <jacksonma at acm.org> wrote:
> > Hoping for illuminating replies, I ask an open question.
> >
> > In the phrase "Correctness by Construction", what does 'correctness'
> mean?
> >
> > -- Michael
> > _______________________________________________
> > The System Safety Mailing List
> > systemsafety at TechFak.Uni-Bielefeld.DE
> > Manage your subscription:
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> > --
> > Yours,
> >
> > Dewi Daniels | Director | Software Safety Limited
> >
> > Telephone +44 7968 837742 | Email dewi.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
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200715/7cf3b1df/attachment.html>