[SystemSafety] Logic

[Heath Raftery]

On 19/02/2014 4:13 AM, Dewi Daniels wrote:
> Derek,
 >
> You also wrote:
>
>> It is also arm-waving to say that formal methods will scale to large
> (i.e., more than a few hundred lines) systems.
>
> I am astonished by this statement. I was personally involved in the program
> proof of several thousand lines of code in the early 1990s, including the
> Full Authority Digital Engine Controller for the Rolls-Royce RB 211-535.
> Since then, there have been many much larger applications of formal methods,
> including SHOLIS, Tokeneer and iFACTS. Furthermore, there has been a
> noticeable reduction in the number of Blue Screens Of Death in Microsoft
> Windows in the large decade; I understand this has, to a large extent, been
> achieved by the adoption by Microsoft of a tool based on formal methods to
> detect defects in third-party device drivers (see e.g.
> http://research.microsoft.com/pubs/70038/tr-2004-08.pdf). I find your
> suggestion that formal methods have not been used on programs of more than a
> few hundred lines to be very surprising.

The first paragraph in the Introduction of that paper is particularly 
telling:

"[Originally] the ultimate goal of formal methods [...] was to [...] 
rigorously prove programs fully correct. While this goal remains largely 
unrealized, many researchers now focus on the less ambitious but still 
important goal of stating partial specifications of program behavior."

I hope I'm not misrepresenting Derek's argument, but it seems to me this 
is the core issue. Derek claims that using formal methods on a small 
slice of a larger project does not constitute an example of formal 
methods scaling to a large project. I'm inclined to agree with Derek's 
contention that formal methods scale very poorly to large projects, and 
this paragraph from the paper backs that up.

I however, still remain hopeful, and look forward to reading more 
examples of large scale use of formal methods.

Heath