[SystemSafety] Correctness by Construction

Olwen Morgan olwen at phaedsys.com
Fri Jul 10 12:12:22 CEST 2020


I agree entirely with what Michael says here. I have known advocates of 
formal methods to be, apparently, completely deaf to this issue.

One example was a risible proposal by a somewhat inept FM neophyte on 
modelling time in communication systems. He proposed a model that used a 
single clock to measure time for all parts of a distributed system. This 
is not exactly a good idea when, as in GPS satellites, those parts may 
be widely separated and moving at relativistically significant speeds 
with respect to each other.

Best, perhaps, for me not to say which particular Phogromping Research 
Group he was affiliated with.


Olwen


On 10/07/2020 10:42, Michael Jackson wrote:
> CbyC is invaluable in avoiding errors in reasoning about formal models. But the relationship of a formal model---whether of a computer or of the real world of a cyber-physical system---may be a more prolific source of faiure. Recent posts cited the 737Max8 disasters. Were these due to formal errors in MCAS code?
>
> -- Michael Jackson
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety


More information about the systemsafety mailing list