[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