[SystemSafety] Logic

[Peter Bernard Ladkin]

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;
entertain-serious-thoughts-of-drowning(-in-alcohol-or-otherwise)

PBL

-- 
Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de