The Abnormal Distribution

Actually, the trope is the second of four topics I wish to address

I recently exchanged opinions with Michael Jackson on the use of mathematics and logic in software development (his main interest) and system safety engineering (mine). If I understand him right, Michael believes that a story must be told about how mathematics and logic applies to clarification of things expressed in natural language, and about how mathematics and logic applies to the world. I have what I believe is a simple, direct story, which comes first.

I believe that people working in system safety engineering often form opinions about use of mathematics and logic which are wrong. These opinions propagate amongst sympathetic hearers, and thereby become tropes. I want to address here one such trope. This comes second.

Third, I comment further about the Hazan I discussed earlier in Progress in Hazard Analysis.

Finally, I say a word about the justification for model-theoretic semantics for first-order logic, as proposed by Alfred Tarski some 75 years ago.

First, the story about applying mathematics and logic. There is some story about how natural language works. I don’t want to suggest here what that story is; just that there is one. Whatever that story may be, I hope it is compatible with some sort of Austinian naive realism, as follows. When I assert “the sky is blue now“, I am referring to a real object, the sky, ascribing to it an objective property, that of being blue, and what I say is true or false, or indeterminate if it approaches a color boundary uniformly (say blue-grey), or it is disproportionately covered with cloud and so on. The story will explain how I refer (to a real object in «the world»), how properties are ascribed, and what counts as success for such an ascription («true») and what as failure («false») with some middle group («indeterminate»).

Exactly the same story, whatever it may be, holds for a formal language. Whatever the story is about how reference works for designatory terms, how property ascription works, how truth and falsity is determined, works the same way for a formal language as it does in natural language. Whatever I can say, and however I can say it, I can also say it formally in just the same way. The only ability I need to be able to say something formally which others might have expressed in natural language is the ability to parse.

Mathematics in its function of applying to the world, and logic similarly, extend the naive view of language expressed by the sky example in that they are schematic ways of doing things. That is, they generalise over concrete instances and demonstrate to us inferences we may perform that lead from true things we know to true things we were not necessarily sure about but now may be sure, after the inference has been performed. I may derive an answer to 456 + 7491 = ??. I may accept A and accept B, and want to know what I can assert about both in one assertion: for example, (A && B), or (A OR B). Alternatively, attempted inferences we wish to make do not go through, for example we know (A OR B) and want to know what this tells us about A (answer: nothing), and we are thereby induced to discover additional truths which may make them go through, or conclude indeed that our wished-for conclusion might be wrong.

Whatever the story is about how all this works, it works with other things also. I know the law forbids me to drive my car immediately after the “30″ sign at 50 kmh, and I do not have to tell myself a complicated story about abstractions and symbols in order to explain the summons that comes in the post after I do so. Few of our fellow citizens who had problems with math and other abstractions in school have difficulty understanding why that summons arrived. So some story of how general schemes work is available to them, without it having to rely on those difficult topics which they could not master in school. Naive realism works for them. For the story about how engineering mathematics works, or business book-keeping for that matter, I am also inclined towards some kind of explanation along the naive-realistic lines proposed by Penelope Maddy some while ago (Realism in Mathematics, Oxford University Press, 1992).

If one doesn’t go for some such account, then it seems to me that the only available alternative is to explain the success of business book-keeping in terms of some sort of tacit convention, as John Searle explained concerning the use of money (The Construction of Social Reality, Penguin, 1995). We somehow “agree” to use arithmetic to come to agreement on transactions. But then the question arises why we use Peano arithmetic (PA), that is, the calculations that are theorems of PA, rather than some other calculations which are not. One can show certain advantages. For example, if I agree with the merchant that I may buy two items and pay him the Peano-sum of the prices, we can merge transactions rather than having to make two separate consecutive ones. But then, a story still has to be told of how PA correctly predicts what change I have in my pocket after either form of transaction, and that this turns out to be the same whether I make the one transaction with the sum, or the two transactions consecutively. PA is obviously more useful than other alternative calculations and a purely-conventional account must explain how this comes to be. A Maddy-type realism account gives a straight answer.

Logic is the science of inference. It says what conclusions follow from what premises because of their form (and how), and provides some methods of determining conclusions that may validly be drawn and those that may not be. It is a science of the use of language. We may and do put it in mathematical terms nowadays for the same reason, I suggest, that Newton was able so to formulate his natural philosophy, and merchants, much earlier, were able to do so for their transactions, and invented 0 to help them. There are certain generalities we discover that may be put in a much more perspicuous and manipulable form by such techniques than if we continue to use our everyday words to work with them. But the principles remain the same. Naive realism suggests that no new story must be told to explain how this works than must be told to explain how language works in general (whatever that might be).

There are some people who want to say “formal logic is not very useful in engineering“. Formal logic is one way of putting the science of inference in manageable terms, and inference is especially useful in engineering, indeed it is one of the main two or three activities in engineering, the others being bending metal and talking to liability lawyers .

Second, the trope. There are some people who want to say “formal logic, say first-order logic, has Tarskian model-theoretic semantics, so one needs to have a model of anything expressed in first-order logic, and this model is mathematical, and mathematical abstractions cannot be a perfect guide to reality; there’s always some misfit“. I see that kind of argument a few times a year and I think it is balderdash (to use another word starting with “b”). Since I see it a few times a year, I conclude it’s a trope. Since it’s balderdash, I conclude it is misleading.

First point: I use first-order logic (FOL) to talk about inferences in language. No one can force a Tarskian semantics on me purely through that use. (I might still want to use one, though, and the final portion of this note explains why.) When I talk about the sky, I have in my FOL-language a term “the-sky” that designates that (here is interpolated the usual story about reference, identical for my NL talk and for my FOL-talk, whatever that story might be). So, in the trope, that step to model-theory fails.

Second point: it is demonstrably not true that there is always some misfit between mathematical “abstractions” and reality. Peano arithmetic tells me exactly what the reality is about monetary transactions. There is no misfit. If one might be worried about Wittgenstein’s point (actually, Kripke’s point which he attributes to Wittgenstein in Wittgenstein On Rules And Private Language, Harvard University Press, 1982) about how one can tell if one is applying a rule, let’s restrict talk about Peano arithmetic and reality to all combinations of transactions in £ and ¢ which lie under £1.

There are a few logical Luddites in system safety, but I don’t know any who go as far as to argue that you always have to remain wary of your demonstrably-correct arithmetical calculations in case the world just doesn’t fit arithmetic exactly. That formalising one’s inferences should be somehow metaphysically suspicious while formalising one’s arithmetic is not seems to me to be plainly inconsistent. If you asked a civil engineer to design a bridge, and heshe gave you a design, and you asked for the engineering calculations, and heshe said “well, we don’t have any, because statics relies on calculus and arithmetic, and calculus relies on arithmetic also, and, well, we are suspicious that arithmetic may not be a helpful guide to the way the world really is“, what would you think? I know what I’d think, and I may be tempted to put it in writing and send it off to the engineering institution that chartered that engineer.

Third, progress (unfortunately not so much) on the Hazan example. The reason I addressed the trope above is that it arose during discussion on the York list of the Hazan example which I treated a couple of notes back in Progress In Hazard Analysis. Here is where we seem to be (to be stuck?) on the example today.

Recall that Daniel Jackson formalised the analysis in Alloy, and found that the initialisation conditions were not addressed in the STPA analysis. Nancy Leveson says in a reply that these conditions are handled later in the book, but does not provide a citation.

Daniel included his analysis in a set of slides he produced for How To Prevent Disasters, his Keynote talk at SIREN//NL in Veldhoven on 2 November 2010. A “more polished” version of the Alloy model is at this associated URL.

I had another question of the STPA analysis, posed in this note: how does one show completeness of the high-level safety requirement? What this meant was not apparent to everyone; for example see Andrew Rae’s response. Translated, using the terms introduced in Formal Definition of the Notion of Safety Requirement, the question means: how do you show that you have captured all the necessary safety properties expressible in the limited vocabulary that you are using at this stage, and not captured more than you need?

If the answer is to be “this is impossible” (the original answer, but possibly misunderstanding the meaning of the question, from this note) then the answer is simply wrong. If the answer is to be “this is not possible in [XYZ proposed Hazan method]” then I would observe that [XYZ proposed Hazan method] forgoes an objective test of its quality, which other methods (such as OHA) have shown how effectively to incorporate.

To date, I have seen no technical answer to the question, despite subsequent discussion about the matter on the York list.

To summarise, (1) Daniel Jackson’s analysis using Alloy showed a weakness of the specific analysis of the example. I am not familiar enough with STPA to know whether it requires a check for initialisations. Since the example evidently did not include one, I would imagine not. If this is so, it seems to be a weakness. (2) It appears that STPA does not explicitly require a check that all necessary safety properties expressible in the vocabulary at a certain development stage have been captured; and no more than necessary. This is possible within certain limitations (indeed OHA shows how to go about it). A method which does not do this foregoes an objective test of its relative success.

Fourth, and finally, the model theory of FOL and its foundations. It was invented by Alfred Tarski in the 1930′s. I met Tarski in the 1970′s (I did my Ph.D. in “his group”, the Group in Logic and the Methodology of Science at U.C. Berkeley). Tarski was very clear that everything he did was science. He treated the subject matter of mathematics as no different from trees or galaxies. As far as he was concerned, he was discovering things about the world. He would have had no patience with people who argued “it’s a model, and models cannot reflect reality perfectly“. I think he would have said “models are reality; just bits of it, not the whole thing“. He thought the encapsulation into models was a form of closed-world assumption in the same way as, when we talk about the vagaries of chess, we do not need to invoke quantum mechanics or the make-up of distant galaxies. I imagine he would have said: in the same way in which if we are talking about the hazards to an A380 aircraft taking off from London Heathrow airport, we do not need to invoke the weather in Beijing. The language of a model is a restriction to what is relevant, no more and no less. And to determine what is relevant we have criteria which are outside the model itself, but which are no less clear for that. So people invoking the trope considered above are also, in my view, being unfaithful to the justification with which model-theoretic semantics for FOL was proposed.

This essay concerns the theory of safety requirements, how they may be defined. I am not concerned here with practical methods of determining them. The concepts here may act as a touchstone for evaluating practical methods of determining safety requirements.

A hazard is defined in Leveson’s text Safeware (Section 9.3, page 177) as a system state (or “set of conditions”) from which, in conjunction with some state(s) of the environmental, an accident will inevitably result. MIL-STD-882D also defines a hazard as «conditions» that somehow may result in an accident. The advantage of Leveson’s definition is that it is precise, when you know what a state is. It is fair to imagine that «condition» refers to state, as contrasted with behavior, which I take to be best construed as a sequence of states, as in the ontology in my on-line book. However, the development here also holds true for hazards construed as sequences of states – behaviors. Any practical aspects, though, thereby become combinatorially much more complex.

Hazard (states), then, are defined. They form a set, HazSt. For all real systems, HazSt is finite, since the set of all system states is finite. It follows that HazSt is describable in a sufficiently expressive formal logic L. That is, HazSt is the unique model (up to isomorphism) of the description in this logic.

From this, we can define the safety requirements. First, for any sentence Q in L, let States(Q) be the set of states in which Q is true. Then the formal safety requirement SafeReq is defined to be the following sentence:

That is, SafeReq is the disjunction of all assertions which define some subset of HazSt. SafeReq is a single sentence (of the sufficiently expressive logic). It is a sentence which defines exactly the complement of HazSt. It is perhaps necessary to note that the way in which SafeReq is defined here gives no clue to its practical determination. For one thing, this definition obviously includes many redundant conjuncts. For this reason, one may take SafeReq to be any logically equivalent sentence to this one.

Now, there are three ways I can think of defining a safety requirement using SafeReq. One is: (a) the system shall never be in a hazard state. Another is: (b) the system may be in a hazard state with likelihood at most P (let’s take a frequentist interpretation: it is in a hazard state up to P proportion of the time, and it is not in a hazard state at least (1-P) proportion of the time). Suppose (c) one wants the probability with which the system may be in a hazard state to depend upon the hazard state. Then one can use the construction which I elaborate, and clause (b) above, for each hazard independently.

So the exact safety requirement is, for a safety requirement of the form (a), SafeReq; for a safety requirement of the form (b), Probability(SafeReq) less-than-or-equal-to (some low likelihood); and for a safety requirement of the form (c), a conjunction of the per-hazard individual safety requirements of form (b).

Completeness is obvious: this is an exact expression, and all of these notions (a), (b), (c) are exact given that SafeReq is. If I have an exact expression of what I need to avoid, that is as good as it can get, theoretically. This expression is dependent, of course, on the definition of the notion of hazard; here, following Leveson’s definition, the notion of hazard is exact, but where it is vague, any notions defined in terms of it will inherit that vagueness.

The same construction also works when we consider hazards to be global states (that is, system state + environment state), when the relevant environmental parameters are state-like. And indeed, one can bring almost any hybrid system into this construal; Leslie Lamport showed how in the nineties in the paper Hybrid Systems in TLA+. The same construction also applies if hazards are environmental states.

One can construe Hazan hereby as an attempt to determine SafeReq in a practical fashion. If one regards OHA as a practical approach to Hazan, as we do, then there is a suitable notion of “the best we can do, logically” at a given stage of the refinement. I assume in readers some understanding of what constitutes a formal refinement using formal languages.

Let L.k be the language of refinement level k. For Q in L.k, note that the refinement in an OHA converges to L (one hopes! Although for combinatorial reasons it will likely never reach it). Let Q.L be the translation of Q in L (indeed, Q.L will normally be identical to Q, since we may assume that L includes L.k). Let States(Q) be the set of states in L (the language of SafeReq, so states-in-L are exact representations of the real states) in which Q.L is true.

I define: Q is a sufficient safety requirement for Level k iff States(Q) superset-of HazSt. Q is a complete safety requirement at Level k if Q is a sufficient safety requirement for Level k, and additionally Q implies all sufficient safety requirements for Level k.

None of this suggests practical ways to achieve or express any of these concepts. But it does show that an exact safety requirement of one’s favorite sort exists in theory, in the sense of being exactly expressible in some sufficiently rich language, for these concepts of hazard and system. It also shows that a Hazan which follows successive formal refinement, such as OHA, has a well-defined notion of sufficiency and completeness of safety requirements for each individual refinement level. Given that these notions of sufficiency and completeness are defined for each refinement level, one may inquire, formally, if one’s identified safety requirements at a given refinement level are sufficient, respectively complete.

This surely renders moot any discussion of whether completeness of safety requirements is “possible”. The question becomes whether achieving exact completeness in Hazan is practically achievable. In particular, for OHA and other refinement-based Hazan methods, the question of completeness of the safety requirements at a given refinement level is exact, and one may well take the view that it should be answered level-by-level in course of the Hazan.

I thank Daniel Jackson for helpful discussion.

I thought up the following parable in order to show the value of particular sorts of formal completeness during hazard analysis (Hazan). Contemporary Hazan strikes me as a procedure or procedures in which clever, knowledgeable people sit down together, think about all the things which can go wrong and list them, and stop when they think they have thought of them all. Various rituals with their various names go with this, but the results are consensual and not necessarily objective, in that important properties of the analysis, such as forms of completeness, are not assessed or assured. Our technique, Ontological Hazard Analysis (OHA) performs Hazan in a formal way which ensures certain objective properties of the resulting analysis, rather than just the consensus arrived at by traditional techniques.

There’s a big apple orchard in the countryside, not far from a big housing estate, and families love to go there and picnic under the trees. But there is a problem.

When the apples fall to the ground, people pick them up and eat them, take them home sometimes. Every so often, one explodes, and people are harmed.

We do have some sort of a test for good apples, ones that will definitely not explode, but most apples we just don’t know about, and it’s not practical to insist that the ones which may explode are cleared up, because there are just, well, way too many. It’s impossible to collect them all up and check them. For one thing, we don’t seem to be able to tell when we have got them all.

The ownership of the apple trees is scattered over many people, and each person’s trees are distibuted over the field, so one can’t, say, put a fence around Joe’s, and a fence around Mary’s trees, and so on.

There is a safety assessor. He (for he is male) comes around at harvest time, and asks all the apple tree owners what they have done to ensure safety. He asks Mary. Well, says Mary, I have this list of exploding-apple experts with decades of experience and CVs longer than the road you took to get here, who came last Friday, looked around in the vicinity of my trees, debated at length using special words I am not very familiar with, and picked up some apples consensually thought to be possibly bad. He talks to Joe. Similar story. Indeed, he talks to all the apple owners.

Then he comes to me. Well, I said, I injected my trees at the beginning of the season with a special substance which gets into the apples, and which I can sense using this magic wand. The wand isn’t very sensitive, but when it pings there is an apple of mine within two meters of it. Now, I used this to pick up all my apples and inspect them. The ones that are obviously good I put back on the ground for people to enjoy. The ones I couldn’t tell, I painted blue and put them all in a basket. Then I put the basket in that bunker over there, so when one explodes no one will be harmed.

That sounds pretty good, agrees the assessor, but how, he asks me, could I possibly have picked up all my apples, for there just seem to be lots and lots? Well, I said, I went to contraption-school and not apple-growing school, so I devised this contraption with 40 arms and sensors. It goes to where my magic wand said there’s an apple. Because, you see, where my magic wand says there is an apple, I know from experience that there’s somewhere between 3 and 37 apples within two meters; there are never more than 37. My contraption picks them all up simultaneously, waves them fast one after the other at the wand, and when the wand peeps loudly, it puts it in that big basket over there. So we do four square meters, accurately, in just a little bit longer than the time it takes to pick up one apple. And we go over all the places near to my trees. So that solves the collection problem.

Then we take the big basket, and do the good/don’t know test, paint the don’t-know’s blue and put them in that blue basket over there. And we put the good ones in that yellow basket. Then we take the blue basket to the bomb bunker, the one over there with Safety Requirement painted on the lintel, and then we chuck the contents of the yellow basket back in the orchard.

That all sounds pretty good, said the assessor, but do I have documentation that all this happened as I said. Sure I do, say I, here it is. And in five minutes looking through it he is convinced.

But why bother doing this? He asks me finally. There are sooooo many apples in this orchard, and yours are only a few of them. You don’t do all of them. I say there are a few reasons. First, if an apple explodes this season and someone gets hurt, then you know right now it’s not one of mine, so that will save you time and resources reinterviewing me about it, and it saves me the cost of possible recompense, because we know in advance ’tain’t one of mine: you’re holding the proof in your hand. Second, you’ve gone round the other growers interviewing them at length and satisfying yourself at length whether the experts they hired really did an adequate job. Whereas, with me, it’s taken you ten minutes and you have proof of adequacy of my measures. That has saved you time, it’s saved me time, so we can go off and do something else with the time we saved, and the evidence you have in hand is better than what you get from the others.

So, he says, why don’t we insist that all do what you do? Well, you probably can’t, say I, because there are sooooooo many apples, and besides not everyone has this lucky property that my trees have, that there are only ever less than 37 apples per four square meters round a tree. But maybe we can hope, says he, that at least some other people will be able to use your technique, and then we can all save a little more time, be a little more sure that more apples are safe, have maybe a couple fewer accidents this year, and all in all improve the quality of our product!

Yes, and why not? say I.

The assessor returns to headquarters and tells his chief, Mr. Golden-Apple-Guru, what he has just seen. Oh, don’t be silly!, says Mr. GAG. That’s all nonsense what Ladkin told you. He can’t have done that. Everyone knows that Completeness Is Impossible! You’re fired!

Key

Many definitions of hazard construe hazards as states. The apples represent states. Whether they are system states, or states of the system+environment, depends on your definition of hazard. MIL-STD-882 and Leveson’s Safeware define hazards as system states.

Hazards are supposed to be conditions in which the chances of an accident are increased. For many conceptions, it is also important (although unstated) that for an accident to happen, the system must pass through a hazard state. (If this condition is not fulfilled, then one exposes oneself to possibly mistaken calculations of risk, as shown in my book chapter Problems Calculating Risk Via Hazard .) The exploding apples, or, rather, their immediate consequences, represent accidents that happen through a hazard state. It is important to note in the parable that all that explodes is an apple.

“My” trees represent those yielding hazards at a particular development stage. In Ontological Hazard Analysis (OHA), these development stages are formal refinements of (earlier) stages. The apples “my” trees shed are the hazards identified at this stage. Daniel Jackson has proposed that HazAn may be performed entirely before one starts on the software development, in this note to the York safety-critical list. Whether this turns out to be so, in the typical OHA there will be many refinement stages before one gets to the point of proceeding with software development.

Daniel has queried the point about knowing there are only at most 37 apples to pick up around «my» trees (private communication). This was my attempt to indicate a level of control imposed during OHA, a deliberated restriction of vocabulary so that the system states may be enumerated (or their relevant equivalence classes may be enumerated) and sorted into hazards and non-hazards as happens in the parable. My special picking tool is intended to show that one applies a specific technique for this sorting at a specific refinement level; we have developed no effective general techniques for so doing and doubt that there are any.

I sent a version of this parable to the University of York safety-critical systems mailing list on 01 November 2010 at 08.33. It was intended to illustrate the values of formal analysis, contrary to claims such as that it is «impossible» to establish completeness of the high-level safety requirements unless you ignore most of the relevant factors, a suggestion which appears in a response of Nancy Leveson to a question of mine in a note in the York thread of 31 October 2010 at 11.15. I believe such claims to be mistaken, but they are also widely believed, as may be seen by reading wider in the thread. Whether the parable helps to counter such claims is, of course, up to the reader to judge.