[SystemSafety] Correctness by Construction

[Olwen Morgan]

On 13/07/2020 14:31, Peter Bernard Ladkin wrote:
>
> As I use the term, source code SC is developed CbyC, it means
>
> * there is a Requirements Specification RS which allows one practically to determine whether certain
> program behaviours fulfil it or not
>
> * there is a means Chk of determining whether program behaviours will satisfy RS through analysis of
> the source code SC of the program and the meaning of SC. (This statement assumes Chk is sound.)
>
> * Chk is incremental, that is, it may be applied soundly to source code as it is being written, and
> relatively comprehensive, that is, it can be applied to most programs SC
>
> * SC is indeed developed with incremental use of Chk

Plus what PBL has here omitted - and without which any attempt at CbyC 
can rapidly fall apart:


1.    Draconian configuration management of all tools used within the 
process and artefacts produced by it.

2.    Validated compilers and, for some languages, draconian language 
subsets.

3.    A suitably capable Chk element supporting *automated* program 
proof. SPARK tools are pretty good but C tools vary. Homo sapiens is 
useless.

4.    In-process review procedures that are fit-for-purpose and strictly 
followed.

6.    A critical mass of suitably trained and supportive staff.

7.    Supportive, technically-aware management that understands what 
CbyC does - and does not - do for them.

8.    Users/clients who are prepared to participate in early life-cycle 
CbyC activities, e.g. walk-throughs of formal specifications in Z.

9.    The right kind of application to deploy it on.

... etc. ...


SPARKies please shoot me down if I'm spouting BS,

Olwen







> PBL
>
> Prof. Peter Bernard Ladkin, Bielefeld, Germany
> Styelfy Bleibgsnd
> Tel+msg +49 (0)521 880 7319  www.rvs-bi.de
>
>
>
>
>
>
> _______________________________________________
> 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/20200713/8f69cfc3/attachment-0001.html>