[SystemSafety] Correctness by Construction

[Peter Bernard Ladkin]

On 2020-07-15 17:14 , Michael Jackson wrote:
> Thank you all for your emails on this topic.
Michael,

I didn't see my view of CbyC reflected in your summary or the discussion. I am also not sure that
the conclusions accurately reflect safety-critical system building or the division of intellectual
labour involved.

No matter what one thinks of such divisions, I think it worthwhile to say what they are and where
they come from. (Those unconcerned about recent history, or about standards in general, can skip the
background below, but it is hard for me to imagine serious commercial developers of safety-critical
systems ignoring standards.)

[Background]

Background to this is that since 2010 I have been actively working through the German
electrotechnical standardisation body DKE to specify what formal methods are industrially mature and
to write a description of their effective use and how they fit together. After 7+ years of
discussion in DKE, that project was proposed to the IEC and approved. This description has been
given the number IEC 61508-3-2. Work is now underway; we are on the second Committee Draft from what
I still imagine will be three.

Safety-related cyberphysical systems are governed (in whatever way you want to take this word) by
IEC 61508, except for medical systems, rail, road, air, nuclear power and probably some other
branches. There are "derivations" of 61508 for other branches, namely industrial processes (the TC
whence 61508 derived) and machinery, which increasingly includes robotics, as well as (forthcoming)
defence industries.

Safety-related systems are necessarily cyberphysical, with one exception, namely ATC data systems.
They are not safety-related according to the applicable definitions because they are infosystems and
communications systems and do not directly physically influence the world to cause harm - such harm
is always mediated (by human operators). They have safety-related functionality, though, if you
consider the wider sociotechnical ATC system including human operators. I call the safety-related
property of an ATC infosystem which passes information which is safety-critical for the
sociotechnical system "semantic safety". Having said that, let me set it aside.

A number of us have been thinking for over a decade now, then, about which bit goes where, when you
are using mathematical and logical methods to develop SW. There is a waterfall-ish chain. Much of
that is given in its essence in my 2011 Ada Connection paper
https://rvs-bi.de/publications/Papers/LadkinAdaConnection2011.pdf

[End of background]

Both IEC 61508 and the civil aircraft certification regs 14 CFR 25 and CS25 consider that
requirements are determined by engineering processes which on the face of it have nothing to do with
SW. In IEC 61508 requirements specification and analysis are in Part 1. Conformant SW development is
Part 3, a separate document. 14 CFR 25 and CS 25 barely mention SW.

CbyC is a term concerning SW development. So if it is to be used a context governed by safety
standards, users will have to separate the CbyC methods they wish to use for requirements from the
CbyC methods they wish to use for SW development. IEC 61508-3-2 separates them implicitly. Of course
there must be and is an interface. In my view, and not just my view, this interface is not
necessarily dealt with very well in either set of standards/regs. (By those working with 61508 it is
often called "requirements traceability".)

So when Martyn and others incorporate requirements elicitation/analysis/validation processes into
CbyC, I see them as conflating what are two nominally different processes in the standards/regs. One
can always say the separation is pointless or inefficient, but the fact is that it both reflects and
determines significant parts of concrete industrial processes and that will be so for the
foreseeable future. It seems helpful, therefore, to separate dependable requirements development
processes from dependable software development processes. That is why my construal of CbyC assumes a
requirements specification, rather than including requirements development in CbyC. Such a
specification, in fact, is what SW developers of safety-related systems are generally given, with
limited opportunity for feedback.

This is not to say there is no feedback from lower in the chain to higher. Wynne Royce showed that
feedback explicitly in his original Waterfall paper. But there is an organisational boundary there
in most developments, which imposes impedance on feedback.

The reason why I stop at source code is that the processes required for veridical conversion of
source into machine code + HW are typically very different processes from those required to derive
dependable source code from given requirements specifications. They are typically executed also by
different organisations.

In order to obtain a dependable system, of course, all three parts (requirements development,
production of SW source code, transformation into physical HW+configuration) have to fit together.
But just as a matter of organisational behaviour, this is not a straight-through process.
Aerodynamicists are not experts in what ways the various microprocessors do and do not execute the
machine code they are said to implement. Compiler writers and maintainers are not expert in
derivation of code from arbitrary requirements specifications.

None of this is to say that I am particularly a fan of the standards and what they constrain. I find
generally much more to criticise in IEC 61508 than I find to praise, and I have lost confidence that
the proposed next edition will be much improved (if at all) over the current 2nd edition, which has
some notable flaws. The aeronautical certification regulations I think are in much better shape
(despite what our MIT colleague likes to opine), but this is in part a consequence of how that
industry works. There is a uniformity of very high interest that what has happened in the past will
not happen again in the future. In the development of IEC 61508 there are different business models
of various industry branches in play which preclude such a uniformity of interest.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
Styelfy Bleibgsnd
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200716/664dacaf/attachment-0001.sig>