[SystemSafety] Correctness by Construction

Wed Jul 15 15:12:58 CEST 2020

Thanks Dewi

So far I have declined the opportunity to comment on this thread as I
simply don't have the time.  Today, I'm on a long webex call, some of which
is interesting, and therefore have some 'spare' time.....or rather
multi-tasking time.

To be clear, D-RisQ Kapture enables English [like] Software High Level
Requirements (HLR) to be written. It helps avoid some of the problems of
writing verifiable HLR, among a bunch of other features.  The D-RisQ
Kapture tool enables an automatic translation to a formal representation
(hidden) which is why it can be useful in both formal and non-formal
developments.  It is currently targeted at control systems and has been
used to describe the behaviour for FCS (as Dewi highlighted) and, among
plenty of other uses, to describe the required behaviour of unmanned
systems.  All aimed at meeting DO-178C/DO-333 Objectives in Table FM.A-3
(it won't meet all of them; some review is needed eg for 'derived
requirements'). It has been used (in the US) in retrospect to find issues
in flight ready code that had failed system test and, in using Kapture,
enabled the discovery of hidden issues which would have meant system
failure in other tests, possibly post delivery given the corner case of one
of the issues discovered (lots of $$$ savings as a result). In future
issues of D-RisQ Kapture, we will be able to automatically check between
requirements that they are [self] consistent, among a few other features.
This assists with CbyC.

We also intend to develop a System Requirements version of the tool;
similar features to Kapture.  This will link to Kapture and will enable a
formal refinement check to be undertaken (automatically).  The System level
tool will have similar features to Kapture.  This effectively will mean
that the English [like] System statements have been correctly and
completely, etc refined into software HLR.  Lots of effort still to come.

If a formal process is to be followed and the design is in
Simulink/Stateflow, we can independently, formally and automatically verify
that the design satisfies the HLR (from Kapture) using the D-RisQ
Modelworks.  Again, this supports various Objectives in DO-333 Table
FM.A-4; in this case it meets all but 3 of the 13 objectives completely,
the remainder are partially met.  Again, supports the notion of CbyC.

CLawZ for C is under development and will independently, formally and
automatically verify automatically produced C code (from OTS coders such as
initially dSPACE TargetLink) against the design.  The template for this
tool is the version we did for Ada some years ago.  It will
enable claims against DO-333 Table FM.A-5 Objectives (all but 2, ignoring
PDI ...for now).  The aim is to have this ready by the end 2020.
Meanwhile, we aim to develop FEVER which will independently, formally and
automatically verify automatically produced EOC (ie the compiled code)
against the source code and enable clams to be made against all but one of
the DO-333 Table FM.A6 Objectives; the remainder will require some manual
test, but not necessarily unit test. Aim is for mid 2021 if all goes
according to plan.  Both tools support CbyC.  Note that the use of all 4
tools gives claims for all but one of the FM.Table A-7 Objectives.

While the above is an overview, I will emphasise that some testing will be
required.  This will not necessarily mean 'unit test', but some other
aspects of checking how the code functions in the hardware will be needed.
Nevertheless, it will significantly speed up development, enable changes to
be inserted quickly and assuredly and certification support given.

Hope that is clear.  If you want to contact me for details of the
technology, please do : njt at drisq.com

Cheers

Nick Tudor
Tudor Associates Ltd
Mobile: +44(0)7412 074654
www.tudorassoc.com

*77 Barnards Green Road*
*Malvern*
*Worcestershire*
*WR14 3LR*
*Company No. 07642673*
*VAT No:116495996*

*www.aeronautique-associates.com <http://www.aeronautique-associates.com>*

On Wed, 15 Jul 2020 at 12:13, Dewi Daniels <dewi.daniels at software-safety.com>
wrote:

> 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
>> >
>>
>> _______________________________________________
> 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/20200715/d866e618/attachment-0001.html>