Skip to Main content Skip to Navigation
Conference papers

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
LAAS - Laboratoire d'analyse et d'architecture des systèmes
2 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : 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.
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download
Contributor : Mohammed Foughali <>
Submitted on : Tuesday, June 11, 2019 - 12:10:19 PM
Last modification on : Thursday, June 10, 2021 - 3:02:06 AM


Files produced by the author(s)


  • HAL Id : hal-02152286, version 1


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⟩



Record views


Files downloads