Statistical Model Checking of Complex Robotic Systems
| Autor: | Cristina Seceleanu, Mohammed Foughali, Félix Ingrand |
|---|---|
| Přispěvatelé: | Équipe Verification de Systèmes Temporisés Critiques (LAAS-VERTICS), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Équipe Robotique et InteractionS (LAAS-RIS), Mälardalen University College, Mälardalen University (MDH), 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 |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
business.industry
Computer science Distributed computing Scale (chemistry) [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering Statistical model 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Formal methods Drone [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] Image (mathematics) Software [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] 0202 electrical engineering electronic engineering information engineering Robot [INFO.INFO-RB]Computer Science [cs]/Robotics [cs.RO] 020201 artificial intelligence & image processing Layer (object-oriented design) business |
| Zdroj: | 26th International SPIN Symposium on Model Checking of Software 26th International SPIN Symposium on Model Checking of Software, Jul 2019, Beijing, China Model Checking Software ISBN: 9783030309220 SPIN HAL |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|