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

[David MENTRÉ]

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é