Re: [SystemSafety] Logic

From: Heath Raftery < >
Date: Wed, 19 Feb 2014 09:10:03 +1100

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.
> 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.


The System Safety Mailing List
systemsafety_at_xxxxxx Received on Tue Feb 18 2014 - 23:10:21 CET

This archive was generated by hypermail 2.3.0 : Fri Feb 22 2019 - 04:17:07 CET