Re: [SystemSafety] Functional hazard analysis, does it work?

From: Peter Bernard Ladkin < >
Date: Thu, 21 Jan 2016 08:50:22 +0100

Hash: SHA256

On 2016-01-20 08:11 , DREW Rae wrote:
> For thirty years advocates of formal methods have shown a total lack of understanding of their
> inherent limitations.

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 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 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

-----BEGIN PGP SIGNATURE----- iQEcBAEBCAAGBQJWoI2+AAoJEIZIHiXiz9k+mmoH/iQB7jkKN/OxoG5XDqxrmZz3 55iyOGto5UZwEQoGmbLZ8e4SvL9M8sEZ0AtTnWqNk8VaUZlUDCugNtENdy1cvWY4 eQtpMrmXpua2nUiXJwVKZMLYrqmFHaqk0jYiJ/Ud77H2uOpPo7GFCGPqS0CR/Nbw 4/5Os5NMwvKDqqZzek9CXHtYnTEPG3tKzom6lzSozB3xI6fGvZNi7ElDiVeP3BWl KoLIWO2BreXsQP9dH/rqI/cqW5052nqTnCQNiAgh/Y7LH2Ir/ovESYJ5HDX3/HQ9 GDiefZ/5Rerqc3k9GHkAKdsgai4zdkBethF0M5pPPvRsbVSGPVEqHtTpKFaG3/o= =Dt/f

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Thu Jan 21 2016 - 08:50:32 CET

This archive was generated by hypermail 2.3.0 : Sat Feb 16 2019 - 09:17:07 CET