[SystemSafety] Correctness by Construction

[Martyn Thomas]

On 15/07/2020 10:49, Peter Bishop wrote:

> The "correctness" achieved by CbyC  does not guarantee that the
> requirements assigned to the software will address the real world problem.

I'm not aware of anything that "guarantees" this. It's not obvious to me
that it is even theoretically possible.

But a CbyC process involves turning an informal specification into a
formal specification. Resolving the ambiguities and internal
inconsistencies in the informal specification necessitates several
detailed discussions with the customer or 'owner' of the requirements.
For a medium sized system there may be hundreds of questions to resolve.
It may be felt necessary to build one or more prototypes or to animate
the specification so that the intended users can review it before design
begins.

None of this provides a guarantee that the requirements assigned to the
software will address the real world problem. If anyone can explain ways
to achieve such a guarantee, I'm confident that CbyC practitioners will
adopt them.  Michael Jackson's Problem Frames are a valuable tool to
reduce the gap between the real world and the specified requirements for
a computer based system and I know they have been adopted by some
developers. See
https://www.researchgate.net/publication/228376733_Problem_analysis_using_small_Problem_Frames,
and
https://people.csail.mit.edu/dnj/teaching/6898/lecture-notes/session8/slides/mj-problem-frames.pdf,
and buy Michael's book!

Martyn