[SystemSafety] Logic

[Martyn Thomas]

On 18/02/2014 22:10, Heath Raftery wrote:
> 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

I think this comment misses the point. Mostly, what you want to be able
to do is to assure particular properties of programs. It's rarely enough
to show that the program fully and correctly implements a functional
specification, as this leaves open all sorts of safety and security
vulnerabilities if (for example) the program encounters input outside
the specified range. (If you disagree with this statement, please send
me a functional specification for a real application that is
sufficiently complete and unambiguous to exclude such issues).

The tools that microsoft use to model-check the behaviour of device
drivers have made a great difference to the reliability of Windows. I
don't think this could have been achieved any other way - years of human
reviewing and testing had proved inadequate to the task.

So let me turn the point round. What would consititute "large-scale use
of formal methods"? and why is the putative lack of such examples
important? Are the "formal methods deniers" really only building systems
for which the smaller scale use of formality would not bring the sort of
benefits that Microsoft, Siemens, Airbus, Boeing, Lockheed Martin and
Praxis have experienced?

Martyn