[SystemSafety] Functional hazard analysis, does it work?

Thu Jan 21 08:50:22 CET 2016

I've heard statements like this for a long time now. I'd call it a meme, but there is more than
one with similar content; it's really a group of memes.

It's very similar, for example, to the meme which says that "advocates of formal methods" make
exaggerated claims about the practical efficacy of their favored methods.

> .. It is the fundamental problem of requirements engineering that strengthening internal 
> validity weakens external validity. .... the rest of us have lost patience with formal gurus
> who don't even admit it's a problem.

Martyn has already addressed the specific issue of formal methods in requirements engineering, so
I am not going to say anything about that, other than refer to this essay
http://www.abnormaldistribution.org/2009/08/16/eight-themes-in-system-safety-engineering/
from five and a half years ago.

What I do want to pick up is the idea that some people have "lost patience" with the exaggerated
claims [or tunnel vision, or whatever the intellectual weakness du jour] of "formal gurus".

Here are a couple of somewhat-detailed examples, and then a conclusion and a question.

Some of us work or have worked in general computer science and software engineering. Exaggerated
claims for software development methods are what you learn to expect. Back in the day, twenty five
years ago, there were the intellectually respectable and highly valued methods of Michael Jackson,
and there were a lot of other methods used widely in industry which solved a tenth of the problems
you needed to solve but were claimed to be comprehensive. Some big industrial clients came to us
because one of them wasn't. Many of the reasons such methods weren't comprehensive is that they
fell over when an industrial issue had a mathematical nature. We solved one: how do you take a
communications-flow diagram with many communicating actors (which the then-current Hatley-Pirbhai
method had our clients construct) and map those functions (and corresponding pseudocode) onto the
hardware, which consisted of a rather smaller number of serial processors? The core issue was
serialisation: how to generate a serial program which veridically executed a network of
interacting agents? Our client did it by hand, and told us it was a huge amount of work about
which Hatley-Pirhai methods gave no clue (talk about eliding problems!). A wizard programmer
working for us suggested a practical solution and built a simulator which seemed to work in cases
where it should. Then Barbara Simons and I spent well over a year after the client project had
ended proving that a somewhat modified algorithm actually did work, the key issue being that it
preserved the communication functions of the original. That was hard combinatorial math. The main
technical problem was that the algorithm wouldn't always work - sometimes the processes simply
couldn't be serialised. We found a straightforward combinatorial test for feasibility, the cases
in which the serialisation algorithm would succeed. (It's all in
http://www.rvs.uni-bielefeld.de/publications/Papers/ladsim-book.ps.gz if anyone's interested.)

This is one example; generalising, my experience with the "formal gurus" with whom I have worked
is rather that we see exaggerated claims made by "software development gurus" (with the notable
exception of MJ) who have handwaved the hard parts, and then we lay in with the math to figure out
precisely what works and what doesn't and when.

That's SW. The hardware industry is no better than software. I went into a computer equipment
supply store yesterday to buy an access point that runs IEEE 802.11ac or IEEE 802.11n, something
that runs in both 2.4GHz and 5GHz bands, to fit in our LAN/WLAN. The salespeople were as usual no
help - "WiFi" is an undifferentiated concept for them (there are actually five different common
protocols, if you count all claimed 802.11n implementations as one). They had an 802.11n access
point, so it says on the box, which I read. Add a wireless network to your wired network. Yep,
that's what access points do and what I want. Get home, open the box, take it out. "Quick
installation". Wait, you have to plug it in via the supplied Ethernet cable to a *computer* on
your wired network. What? You can't just connect it to your router? Nope (believe me, I tried).
So, the next question: who has a computer with *two* Ethernet ports, one for the connection to the
router and one for the connection to the access point? None of the Apple kit we have has two
ports. I conclude that, despite what it says on the box, this piece of kit is not a general access
point. It is an access point for certain limited configurations of home kit and it doesn't say
that on the box.

The point is that BS is pervasive in software and computing at all levels, in all areas. Of course
it is. There is real money to be made in digital computing and people keen to make it, who elide
the technical limitations of their methods in order to sell you stuff. Whether you are amateur or
professional. You can't even call it a peril of capitalism - there were no worse exaggerators of
capability of any sort than the Soviet Union, Communist China and North Korea. It's just what
people do.

I think of valued colleagues who use and advocate mathematical methods in computer and software
engineering: say, Leslie Lamport, John Rushby, Friedrich von Henke, Fred Schneider, Kevin
Driscoll, Martyn Thomas, Rod Chapman. In thirty years, I don't think I have ever heard an
exaggerated claim, or seen an attempt to elide a technical problem (although of course there are
plenty of conjectures which turn out to be mistaken; that's in the nature of the exercise).
Indeed, these are people who go searching for the problems, deliberately. And then solve them. And
prove that they've solved them. As I like to think I do.

So I'd like to know why it is that "advocates of formal methods" are *particularly* singled out,
anonymously, for complaint, when a large portion of the industry lives through exaggeration of its
capabilities.

In particular, I would like to see some actual quotations from respected advocates of formal
methods in software or systems engineering in the last thirty years which exaggerate capabilities
or ignore known problems. (Restriction: let's please leave AI out of this :-) ) If what Andrew
says is true, such quotations should be all over the place. Does anyone have even one?

PBL

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