Skip to Main content Skip to Navigation

Formal verification of the functionnal layer of robotic and autonomous systems

Mohammed Foughali 1
1 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : The goal of this thesis is to add to the efforts toward the long-sought objective of secure and safe robots with predictable and a priori known behavior. For the reasons given above, formal methods are used to model and verify crucial properties, with a focus on the functional level of robotic systems. The approach relies on automatic generation of formal models targeting several frameworks. For this, we give operational semantics to a robotic framework, then several mathematically proven translations are derived from such semantics. These translations are then automatized so any robotic functional layer specification can be translated automatically and promptly to various frameworks/languages. Thus, we provide a mathematically correct mapping from functional components to verifiable models. The obtained models are used to formulate and verify crucial properties (see examples above) on real-world complex robotic and autonomous systems. This thesis provides also a valuable feedback on the applicability of formal frameworks on real-world, complex systems and experience-based guidelines on the efficient use of formal-model automatic generators. In this context, efficiency relates to, for instance, how to use the different model checking tools optimally depending on the properties to verify, what to do when the models do not scale with model checking (e.g. the advantages and drawbacks of statistical model checking and runtime verification and when to use the former or the latter depending on the type of properties and the order of magnitude of timing constraints).
Complete list of metadata

Cited literature [161 references]  Display  Hide  Download
Contributor : Abes Star :  Contact
Submitted on : Thursday, March 26, 2020 - 9:29:11 AM
Last modification on : Thursday, June 10, 2021 - 3:02:06 AM
Long-term archiving on: : Saturday, June 27, 2020 - 12:56:04 PM


Files produced by the author(s)


  • HAL Id : tel-02080063, version 2


Mohammed Foughali. Formal verification of the functionnal layer of robotic and autonomous systems. Logic [math.LO]. INSA de Toulouse, 2018. English. ⟨NNT : 2018ISAT0033⟩. ⟨tel-02080063v2⟩



Record views


Files downloads