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

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


Hello,

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:

   http://toccata.lri.fr/gallery/ClockDrift.en.html

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 : Fri Apr 19 2019 - 12:17:07 CEST