Re: [SystemSafety] Logic

From: Peter Bernard Ladkin < >
Date: Mon, 17 Feb 2014 13:49:46 +0100

On 2014-02-17 12:18 , Martyn Thomas wrote:
> I would be interested to know whether the academics on this list use formal methods to design the
> programs that they write for themselves.

Good question!

I just wrote up ours (plus my thesis experience). Essentially nine products in nineteen years (I only include significant pieces of SW). Plus my thesis work. Here's a summary.

Four using FM. All stand-alone. All essentially flawless. Some comments: 1. One "feature" was found inside a couple hours by the integrator of my thesis work into a larger system. I fixed it; the code worked apparently flawlessly for a third party for a number of years; 2. A provably-correct interpreter for the linguistic-analysis language DATR. The author implemented SOS rules as Isabelle inferences. So of course it works! (subject to Isabelle's soundness. Indeed, it works provably correctly even if the SOS rules have typos - it just wouldn't interpret DATR in that case. But they don't. Many eyeballs have seen to it); 3. An archiving system, VDAS, written in Java and specified using denotational semantics. Specifying the semantics took 2/3-3/4 of the time, with weekly inspections in a group including me. The resulting system worked functionally-flawlessly in one system for us, and formed the basis for a successful two-person SW business for its author for many years. (I say "functionally-flawlessly" because we had to interface other code to it under various versions of various operating systems, and that is irreducibly painful. See below). 4. A communications system derived through formal refinement from a provably-correct very-high-level specification into SPARK. Obviously it works (again subject to the soundness of the SPARK toolset)!

Another five were projects which involved interfacing a large third-party graphics package whose interfaces to modern OSs are no longer maintained, and whose Java interface is "featureful" and appears to be poorly maintained nowadays. Some of these, standalone with clean interfaces for particular OS versions, worked very well, one of them flawlessly. Others were a maintainance nightmare. If you have SW written in scripting languages which use large third-party packages occasionally with other-party interfaces and you want them to work on all versions of Mac OS, Linux and Windows, it appears to be a nightmare and I don't see how any current FM would help at all.

If there were rigorous interface specifications for all these versions of OSs/packages/interface-SW I can see very well how FM could help enormously! But there aren't.

This history should give a hint of why I think that people who say "FM doesn't work" are

self-applying a successful ad-hominem argument :-) My experience over a quarter century has been:
IF largely-stand-alone-SW THEN use-FM; celebrate-success ELSE
bemoan-nightmare-of-package/interface/OS-version-maintenance; endure-nightmare;


Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319

The System Safety Mailing List
Received on Mon Feb 17 2014 - 13:49:57 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST