[SystemSafety] Proving clock-drift related code (Patriot example)

From: David MENTRÉ < >
Date: Tue, 05 May 2015 06:02:17 +0200


Le 2015-05-04 22:57, Steve Tockey a écrit :
> Can static analysis catch this kind of defect:
> https://www.ima.umn.edu/~arnold/disasters/patriot.html
> <https://www.ima.umn.edu/%7Earnold/disasters/patriot.html>

I don't think there is a sound static analysis tool that automatically find this kind of defect (that was my point regarding the 787 overflow bug).

But yes using static analysis tool and some manual coding of the required properties and invariant you can automatically prove needed bounds on such computations:


Best regards,
D. Mentré

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Tue May 05 2015 - 06:02:25 CEST

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:07 CEST