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 [Toulouse]
2 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes [Toulouse]
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 metadatas

Cited literature [39 references]  Display  Hide  Download

https://hal.laas.fr/hal-02152286
Contributor : Mohammed Foughali <>
Submitted on : Tuesday, June 11, 2019 - 12:10:19 PM
Last modification on : Monday, July 15, 2019 - 3:58:11 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02152286, version 1

Citation

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⟩

Share

Metrics

Record views

100

Files downloads

50