[SystemSafety] Correctness by Construction

Olwen Morgan olwen at phaedsys.com
Tue Jul 14 12:31:52 CEST 2020


On 14/07/2020 10:54, Michael Jackson wrote:
> (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.

No. I meant more than that. By input and output predicates, I meant that 
the black-box behaviour of each software element for which verification 
pre- and post-conditions are given to enable the verifier to infer what 
the behaviour is. Sorry if I didn't make it clear.

>   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.)
This gets to the distinction between CbyC and User Acceptance. CbyC is 
intended to help you do the thing right. User Acceptance testing is 
still needed to check that you've done the right thing.
> <snip>
> (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.

Indeed. It's a question of divide-and-rule. Ideally, you bring the 
strongest leverage you can to bear on determining at each stage of the 
process whether or not you have made any errors. CbyC (plus the 
supporting elements of the software engineering process) does that for 
the production of the code. ... And that's all it does.


Olwen




More information about the systemsafety mailing list