A classic approach for critical systems is to have monitoring mechanisms independent of the main control chain, aimed at preventing the occurrence of catastrophic failures. These mechanisms implement on-line checks, and trigger safety interventions when a dangerous situation is observed. Such an approach has already been adopted for autonomous systems, but the specification of safety rules (which intervention to launch?, when?) is typically ad hoc. What's more, existing safety monitors only consider a very limited set of interventions, such as an irreversible power failure. One motivation for our work was to develop a formal approach for specifying safety rules, and to be able to take into account a richer set of temporary interventions, which can be activated and deactivated depending on the state of the system. While ensuring safety, the rules must be sufficiently permissive to allow the system to perform its functions. For example, a mobile robot must always retain the possibility of reaching states where its speed is non-zero, thus enabling its movement function.

The SMOF (Safety Monitoring Framework) method, and the supporting tool of the same name, have been developed to meet these needs[1]. The method starts with a HAZOP-type risk analysis, and uses formal verification techniques to synthesize safety rules. The synthesis algorithm takes into account both safety and permissiveness requirements (the latter being attainability properties in state space). The principle is to associate interventions with alert states, i.e. states that must be crossed before an invariant is violated. Alert state/intervention associations are explored using a branch-and-bound algorithm, which makes calls to the NuSMV model checker to check cut criteria or confirm that a safe and permissive solution has been obtained. An alternative implementation used the notion of a formal game between the safety monitor and an adversary, but this was not adopted for performance reasons[2]. The support tool provides a NuSMV modeling pattern to facilitate the definition of unsafe behaviors in the absence of the monitor and propose candidate interventions with their preconditions and effects. Alert states are automatically identified as predecessors of catastrophic states.

The tool also provides support for producing permissiveness properties. By default, it considers generic reachability properties, but the user can also model properties specific to the needs of the application[3]. This is very useful in practice, as the lack of a solution often stems from the difficulty of maintaining generic permissiveness, which is very demanding. A recent extension concerns the addition of a diagnostic aid, for the analysis of safe but insufficiently permissive security rules. Finally, we have studied how to automatically suggest new interventions to be injected into the synthesis process, to solve these permissiveness problems.

SMOF has been applied to various robots developed by industrial partners: a manufacturing robot (Kuka), an airport maintenance robot (Sterela), and an agricultural robot for livestock feeding (Kuhn).

[1] Machin M., Guiochet J., H. Waeselynck, Blanquart J-P. , Roy M.,Masson  L., “SMOF - a Safety Monitoring Framework for Autonomous Systems”, IEEE Transactions on Systems, Man, and Cybernetics: Systems, Vol. 48, no. 5, pp. 702-715, 2018

[2] Machin M., Dufossé F., Guiochet J., Powell D., Roy M., Waeselynck H.,”Model-checking and Game Theory for the Synthesis of Safety Rules”, 16th IEEE International Symposium on High Assurance Systems Engineering (HASE 2015), Daytona Beach, Florida, USA, 2015

[3] Masson L., Guiochet J., Waeselynck H., Cabrera K., Cassel S., Törngren M., “Tuning Permissiveness of Active Safety Monitors for Autonomous Systems”, Tenth NASA Formal Methods Symposium (NFM 2018), Springer LNCS 10811, pp.333-348, 2018