[SystemSafety] Static Analysis

[David MENTRE]

Hello Peter,

Le 25/02/2014 21:40, Peter Bernard Ladkin a écrit :
> As the article points out, a simple automated reachability analysis
> would have highlighted the anomaly.

But one needs to review the result of the analysis, or determine a 
criteria (e.g. over a given number of lines of dead code) to send an 
error (without too many or no false positive, otherwise the error report 
won't be used). And this should be integrated within the development 
process (e.g. check before releasing a new version). The devil is in the 
detail.

> Note that it has been out there
> in the open for a while - the code is open source.

Which show that without adequate manual or automated review, having code 
(being open source or proprietary) does not help.

On a more positive note, yes having open-source code can allow some 
formal verification by third parties, like for PolarSSL library:
   http://blog.frama-c.com/index.php?post/2014/02/23/CVE-2013-5914

Sincerely yours,
david