Skip to Main content Skip to Navigation
Technical Reports

On the Semantics of the GenoM3 Framework

Mohammed Foughali 1 Silvano Dal Zilio 1 Félix Ingrand 2
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
2 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : The goal of this document is to add to the efforts toward the long-sought objective of secure and safe robots with predictable and a priori known behavior. For this, we give operational semantics to GenoM3, a robotic framework, in terms of timed transition systems TTS. Then, a mathematically proven translation to timed automata extended with urgencies and data DUTA is derived from such semantics. Thus, we provide a mapping from functional components to verifiable models. Since TTS and DUTA are at the heart of a large corpus of formal verification languages and tools (such as UPPAAL, Fiacre, and RT-BIP), the semantics and its translation allow a correct mapping between GenoM3 and such languages/tools. This connection can then be automatized thanks to GenoM3 templates
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Mohammed Foughali Connect in order to contact the contributor
Submitted on : Thursday, January 24, 2019 - 2:37:42 PM
Last modification on : Wednesday, November 3, 2021 - 6:51:53 AM


Files produced by the author(s)


  • HAL Id : hal-01992470, version 1


Mohammed Foughali, Silvano Dal Zilio, Félix Ingrand. On the Semantics of the GenoM3 Framework. Rapport LAAS n° 19036. 2019. ⟨hal-01992470⟩



Record views


Files downloads