Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots
| Autor: | Anthony Mallet, Silvano Dal Zilio, Félix Ingrand, Mohammed Foughali, Bernard Berthomieu |
|---|---|
| Přispěvatelé: | Équipe Robotique et InteractionS (LAAS-RIS), 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 Verification de Systèmes Temporisés Critiques (LAAS-VERTICS), Service Informatique : Développement, Exploitation et Assistance (LAAS-IDEA), European Project: 644400,H2020,H2020-ICT-2014-1,CPSELabs(2015), 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) |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Model checking
0209 industrial biotechnology Robotic software formal methods Computer science business.industry Distributed computing Robotics 02 engineering and technology Autonomous robot Formal methods 020901 industrial engineering & automation Formal specification 0202 electrical engineering electronic engineering information engineering Robot [INFO.INFO-RB]Computer Science [cs]/Robotics [cs.RO] 020201 artificial intelligence & image processing Artificial intelligence business Formal verification Robotics middleware |
| Zdroj: | Proceedings of the 18th International Conference on Formal Engineering Methods 18th International Conference on Formal Engineering Methods (ICFEM 2016) 18th International Conference on Formal Engineering Methods (ICFEM 2016), Nov 2016, Tokyo, Japan Lecture Notes in Computer Science Lecture Notes in Computer Science-Formal Methods and Software Engineering HAL Formal Methods and Software Engineering ISBN: 9783319478456 ICFEM |
| ISSN: | 0302-9743 1611-3349 |
| Popis: | International audience; Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|