Statistical Model Checking of Complex Robotic Systems

Mohammed Foughali (1) , Félix Ingrand (2) , Cristina Seceleanu (3)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
2 LAAS-RIS - Équipe Robotique et InteractionS
3 Mälardalen University College

Failure of robotic software may cause catastrophic damages. In order to establish a higher level of trust in robotic systems, formal methods are often proposed. However, their applicability to the functional layer of robots remains limited because of the informal nature of specifications, their complexity and size. In this paper, we formalize the robotic framework G en oM3 and automatically translate its components to UPPAAL-SMC, a real-time statistical model checker. We apply our approach to verify properties of interest on a real-world autonomous drone navigation that does not scale with regular UPPAAL.

Domaines: Robotique [cs.RO]; Informatique et langage [cs.CL]; Génie logiciel [cs.SE]; Logique en informatique [cs.LO]; Théorie et langage formel [cs.FL]

Mohammed Foughali, Félix Ingrand, Cristina Seceleanu. Statistical Model Checking of Complex Robotic Systems. 26th International SPIN Symposium on Model Checking of Software, Jul 2019, Beijing, China. ⟨hal-02152286⟩