Specifying Safety Monitors for Autonomous Systems using Model-checking

International audienceAutonomous 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