Re: [SystemSafety] Logic

From: Martyn Thomas < >
Date: Tue, 18 Feb 2014 22:31:18 +0000


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



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

This archive was generated by hypermail 2.3.0 : Mon Apr 22 2019 - 19:17:07 CEST