[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