Model-Checking and Game theory for Synthesis of Safety Rules

Mathilde Machin (1) , Fanny Dufossé (1) , Jérémie Guiochet (1) , David Powell (1) , Matthieu Roy (1) , Hélène Waeselynck (1)

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

Ensuring that safety requirements are respected is a critical issue for the deployment of hazardous and complex reactive systems. We consider a separate safety channel, called a monitor, that is able to partially observe the system and to trigger safety-ensuring actuations. We address the issue of correctly specifying such a monitor with respect to safety and liveness requirements. Two safety requirement synthesis programs are presented and compared. Based on a formal model of the system and its hazards, they compute a monitor behavior that ensures system safety without unduly compromising system liveness. The first program uses the model-checker NuSMV to check safety requirements. These requirements are automatically generated by a branch-and-bound algorithm. Based on a game theory approach, the second program uses the TIGA extension of UPPAAL to synthesize safety requirements, starting from an appropriately reformulated representation of the problem.

Mots clés: Model checking; Game theory; Supervisor syn-thesis; Safety Monitoring; Safety Rules; Reactive Systems

Domaines: Calcul parallèle, distribué et partagé [cs.DC]

Mathilde Machin, Fanny Dufossé, Jérémie Guiochet, David Powell, Matthieu Roy, et al.. Model-Checking and Game theory for Synthesis of Safety Rules. 2015 IEEE 16th International Symposium on High Assurance Systems Engineering (HASE), Jan 2015, Daytona Beach Shores, United States. pp.36-43, ⟨10.1109/HASE.2015.15⟩. ⟨hal-01164981⟩