[SystemSafety] Correctness by Construction

[Michael Jackson]

Olwen, Bev, Martyn, Peter, and Peter: 

Thank you for your replies to my question about the meaning of the phrase "Correctness by Construction". As Martyn expected, the replies have stimulated some responses from me and some further questions arising from my understanding (or, of course, misunderstanding!) of your replies. I hope you will be willing to provide further answers, explanations, rebuttals, or whatever is needed. 

First, these are the [abbreviated] direct answers defining or characterising the phrase "Correctness by Construction":

1.  "Total correctness with respect to input and output predicates." (I read 'total' here to include both termination and functional totality over the set of possible input traces.)

2.  "90% fewer defects in delivered software-based systems."

3.  "Incrementally showing, by checking source code, that [all possible] program behaviours satisfy a Requirements Specification."

4.  "The implementation satisfies the specification and does not do anything else." 

Second, some comments on the definitions: 

(a)  These definitions all concern execution of the code that will run on the processor hardware in system operation. (Comments accompanying some definitions also emphasise the critical role of correctness of the compiler, configuration and correctness of other development tools, and correctness of the processor hardware with respect to the hardware execution semantics, 

(b)  In some cases, the emphasis on software execution is salient. The 'input and output predicates' are (I am assuming) inputs and outputs at the ports of the processor hardware. The Requirements Specification is to be satisfied by 'program behaviours' (I am assuming that these behaviours are strictly behaviours of the program as executed in the processor hardware.) 

(c)  In some cases, there seems to be explicit recognition of the physical problem world outside the processor hardware. '[Is the] specified behaviour actually what is needed for the application?' 'There is a Requirements Specificiation'. The goal of 90% reduction in defects is in 'delivered software-based systems'. 

(d)  In addition to 'source code' and 'binary code', other terms used are 'specification' and 'requirement'. There is a reference to 'early life-cycle CbyC ... formal specifications in Z'. In another, '... program behaviours fulfil a Requirements Specification' seems to suggest that the subject matter of requirements is program execution. But there is little description of specifications and requirements. More description and explanation of their form and content is needed, please.

(e)  'Software-based' systems in general, and cyber-physical systems in particular, are bipartite. One part is the software itself, executed solely by the processor hardware; the other part is the governed physical 'problem world' outside the computer. If Correctness by Construction is applied only to the software itself, it can achieve only a limited reduction of system defects. 

(f)  In a cyber-physical system the core development product is the behaviour of the whole system, emerging from the interaction of both of its parts. Development is indeed a programming task, but it is programming the whole system, not just the software part. The heterogeneous nature of the system---quasi-formal software joined with the non-formal problem world---poses a real difficulty. But erecting a logical firewall between the two parts and treating them in effective isolation is not a perfect solution. 

-- Michael