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.