Skip to Main content Skip to Navigation
Conference papers

On Reconciling Schedulability Analysis and Model Checking in Robotics

Mohammed Foughali 1
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : The challenges of deploying robots and autonomous vehicles call for further efforts to bring the real-time systems and the formal methods communities together. In this paper, we discuss the practicality of paramount model checking formalisms in implementing dynamic-priority-based cooperative schedulers, where capturing the waiting time of tasks has a major impact on scalability. Subsequently , we propose a novel technique that alleviates such an impact, and thus enables schedulability analysis and verification of real-time/behavioral properties within the same model checking framework, while taking into account hardware and OS specificities. The technique is implemented in an automatic translation from a robotic framework to UPPAAL, and evaluated on a real robotic example.
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download
Contributor : Mohammed Foughali <>
Submitted on : Monday, November 4, 2019 - 5:17:07 PM
Last modification on : Thursday, June 10, 2021 - 3:06:38 AM
Long-term archiving on: : Wednesday, February 5, 2020 - 11:13:42 PM


Files produced by the author(s)


  • HAL Id : hal-02346015, version 1


Mohammed Foughali. On Reconciling Schedulability Analysis and Model Checking in Robotics. MEDI Workshops. 9th International Conference on Model and Data Engineering, Oct 2019, Toulouse, France. ⟨hal-02346015⟩



Record views


Files downloads