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 metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.laas.fr/hal-01992470
Contributor : Mohammed Foughali <>
Submitted on : Thursday, January 24, 2019 - 2:37:42 PM
Last modification on : Thursday, March 5, 2020 - 2:44:28 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01992470, version 1

Citation

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

Share

Metrics

Record views

102

Files downloads

165