Specifying Safety Monitors for Autonomous Systems using Model-checking

Mathilde Machin (1) , Fanny Dufossé (1) , Jean-Paul Blanquart (2) , Jérémie Guiochet (1) , David Powell (1) , Hélène Waeselynck (1)

1 LAAS-TSF - Équipe Tolérance aux fautes et Sûreté de Fonctionnement informatique
2 ASTRIUM

Autonomous systems operating in the vicinity of humans are critical in that they potentially harm humans. As the complexity of autonomous system software makes the zero-fault objective hardly at- tainable, we adopt a fault-tolerance approach. We consider a separate safety channel, called a monitor, that is able to partially observe the sys- tem and to trigger safety-ensuring actuations. A systematic process for specifying a safety monitor is presented. Hazards are formally modeled, based on a risk analysis of the monitored system. A model-checker is used to synthesize monitor behavior rules that ensure the safety of the monitored system. Potentially excessive limitation of system functional- ity due to presence of the safety monitor is addressed through the notion of permissiveness. Tools have been developed to assist the process.

Mots clés: autonomous robots; safety rules; safety monitoring

Domaines: Informatique [cs]; Robotique [cs.RO]

Mathilde Machin, Fanny Dufossé, Jean-Paul Blanquart, Jérémie Guiochet, David Powell, et al.. Specifying Safety Monitors for Autonomous Systems using Model-checking. International Conference on Computer Safety, Reliability and Security (SafeComp 2014), Sep 2014, Florence, Italy. ⟨hal-01207152⟩