Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics

Autor: Pierre-Emmanuel Hladik, Mohammed Foughali
Přispěvatelé: VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), É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, Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS), Université Toulouse 1 Capitole (UT1)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), 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)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), VERIMAG [2020-....] (VERIMAG - IMAG [2020-....]), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2020-....] (UGA [2020-....])-Institut polytechnique de Grenoble - Grenoble Institute of Technology [2020-....] (Grenoble INP [2020-....]), Université Grenoble Alpes [2020-....] (UGA [2020-....]), Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-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)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse 1 Capitole (UT1)-Université Toulouse - Jean Jaurès (UT2J)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse 1 Capitole (UT1)-Université Toulouse - Jean Jaurès (UT2J), 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í: 2020
Předmět:
Zdroj: Journal of Systems Architecture
Journal of Systems Architecture, Elsevier, 2020, 111, pp.101817. ⟨10.1016/j.sysarc.2020.101817⟩
Journal of Systems Architecture, 2020, 111, pp.101817. ⟨10.1016/j.sysarc.2020.101817⟩
ISSN: 1383-7621
DOI: 10.1016/j.sysarc.2020.101817⟩
Popis: International audience; The challenges of deploying robots and autonomous vehicles call for further efforts to bridge the gap between the robotics, the real-time systems and the formal methods communities. Indeed, with robots being more and more involved in costly missions and contact with humans, a rigorous formal verification of their behavior in the presence of various real-time constraints is crucial. In order to increase our trust in its results, such verification should be carried out on models that are the closest possible to reality, and thus take into account hardware and OS specificities such as the number of cores provided by the robotic platform and the scheduling policy. In this paper, we propose a novel binary-search-inspired technique that allows to extend timed automata models of robotic specifications with dynamic-priority schedulers. Given a number of cores, the extended models can then be checked against various real-time and behav-ioral properties, including schedulability, within the same model checking framework. Our technique is implemented in an automatic translation from a robotic framework to UPPAAL, and evaluated on a real robotic case study, where it shows a significant gain in scalability as opposed to the counting technique used in the literature.
Databáze: OpenAIRE
Externí odkaz: