Safety and hazard analysis in concurrent systems

Safety is a well-known and important class of property of software programs, and of systems in general. The basic notion that informs this work is that the time to think about safety is when it still exists but could be lost. The notion is not just to analyse safety as existing or not with a given system state, but also in the sense that a system is presently safe but becoming less so. Safety as considered here is not restricted to one type of property, and indeed for much of the discussion it does not matter what types of measures are used to assess safety.

The work done here is for the purpose of laying a theoretical and mathematical foundation for allowing static analyses of systems to further safety. This is done using tools from lattice theory applied to the poset of system states partially ordered by reachability. Such analyses are common (e.g., with abstract interpretations of software functioning) with respect to other kinds of systems, but there does not seem to exist a formalism that permits them specifically for safety.

Using the basic analytical tools developed, a study is made of the problem of composing systems from components. Three types of composition: direct sum, direct product, and exponentiation---are noted, and the first two are treated in some depth. It is shown that the set of all systems formed with the direct sum and direct product operators can be specified by a BNF grammar. A three-valued ``safety logic'' is specified, using which the safety and fault-tolerance of composed systems can be computed given the system composition. It is also shown that the set of all systems also forms separate monoids (in the sense familiar to mathematicians), and that other monoids can be derived based on equivalence classes of systems.

The example of a train approaching a railroad crossing, where a gate must be closed prior to the train's arrival and opened after its exit, is considered and analysed as an example.