Statistical Model Checking of Complex Robotic Systems
In: 26th International SPIN Symposium on Model Checking of Software ; https://hal.laas.fr/hal-02152286 ; 26th International SPIN Symposium on Model Checking of Software, Jul 2019, Beijing, China, 2019
Online
Konferenz
Zugriff:
International audience ; 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.
Titel: |
Statistical Model Checking of Complex Robotic Systems
|
---|---|
Autor/in / Beteiligte Person: | Foughali, Mohammed ; Ingrand, Félix ; Seceleanu, Cristina ; Équipe Verification de Systèmes Temporisés Critiques (LAAS-VERTICS) ; Laboratoire d'analyse et d'architecture des systèmes (LAAS) ; Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1) ; Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3) ; Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP) ; Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1) ; Université Fédérale Toulouse Midi-Pyrénées ; Équipe Robotique et InteractionS (LAAS-RIS) ; Mälardalen University College ; Mälardalen University (MDH) |
Link: | |
Zeitschrift: | 26th International SPIN Symposium on Model Checking of Software ; https://hal.laas.fr/hal-02152286 ; 26th International SPIN Symposium on Model Checking of Software, Jul 2019, Beijing, China, 2019 |
Veröffentlichung: | HAL CCSD, 2019 |
Medientyp: | Konferenz |
Schlagwort: |
|
Sonstiges: |
|