[SystemSafety] Correctness by Construction

[Olwen Morgan]

On 14/07/2020 20:20, David Crocker wrote:
<snip>
>
> include a model of the external physical system in the requirements 
> specification. It is then possible to reason and construct proofs 
> about the combined behaviour of the software + physical system, 
> including the effects of external inputs. This approach is in 
> principle applicable to other tool-supported formal specification 
> languages, for example Z.
>
> Although this is conceptually simple, the problem lies in constructing 
> a model of the physical system and possible external inputs that is 
> sufficiently accurate and complete to make the proofs meaningful and 
> useful.
>
Just so. And in my experience an even greater problem lies in the 
difficulty of persuading people that it is, in some cases , necessary. I 
once walked out of and blew the whistle on a train safety project where 
fellow engineers ignored me on this issue.


Olwen