Decomposing the model-checking of mobile robotics actions on a grid

Abstract : Mobile automated systems, such as robots or machinery for precision agriculture, may be designed to perform actions that vary in space according to information from sensors or to a mission map. To be reliable, the design process of such systems should involve the combined verification of spatial and dynamic properties. We consider here CTL model-checking of a mobile robot's behavior, using the UppAal Timed Automata verifier. We consider reachability properties including path finding. Space is modeled as a 2D grid and the mobile robot path is unknown a priori. In this case, the exhaustive state space exploration of model-checking leads to the generation of many possible movements. This exposes such model-checking to combinatorial issues depending on the grid size and the complexity of system dynamics. In this paper, we propose a decomposition methodology reducing the memory requirements for the verification task. The decomposition is twofold. The grid is decomposed in sub-grids and the model-checking query on the whole grid is decomposed in a set of queries on the sub-grids. A set of test cases and check the validity of the decomposition concept. The decomposition methodology is compared to a simpler method that verifies the reachability property without proceeding to decomposition.
Type de document :
Communication dans un congrès
20th World Congress of the International Federation of Automatic Control (IFAC 2017 WC), Jul 2017, Toulouse, France. 2017
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal-lirmm.ccsd.cnrs.fr/lirmm-01592588
Contributeur : Karen Godary-Dejean <>
Soumis le : lundi 25 septembre 2017 - 10:37:39
Dernière modification le : jeudi 24 mai 2018 - 15:59:23
Document(s) archivé(s) le : mardi 26 décembre 2017 - 12:48:14

Fichier

IFAC_2017_VersionFinale.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : lirmm-01592588, version 1

Citation

Rim Saddem, Olivier Naud, Karen Godary-Dejean, Didier Crestani. Decomposing the model-checking of mobile robotics actions on a grid. 20th World Congress of the International Federation of Automatic Control (IFAC 2017 WC), Jul 2017, Toulouse, France. 2017. 〈lirmm-01592588〉

Partager

Métriques

Consultations de la notice

254

Téléchargements de fichiers

72