Found an issue? Give us feedback

Hal-Diderot; HAL-INS...arrow_drop_down

Hal-Diderot; HAL-INSA Toulouse

Other ORP type . 2019

Data sources: Hal-Diderot; HAL-INSA Toulouse

Select content type to embed

All Research products

arrow_drop_down

<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

Claim

On the Semantics of the GenoM3 Framework

Name: On the Semantics of the GenoM3 Framework
Keywords: formal methods, timed automata, [INFO.INFO-RB]Computer Science [cs]/Robotics [cs.RO], [INFO]Computer Science [cs], Robotics, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], transition systems, verification, semantics

appsOther research productkeyboard_double_arrow_right Other ORP type 24 Jan 2019 France English HAL CCSD

Authors: Foughali, Mohammed; Dal Zilio, Silvano; Ingrand, Félix;

On the Semantics of the GenoM3 Framework

- Summary
- Subjects
- References
  (9)
- Metrics

Abstract

International audience; 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

Country

France

Related Organizations

Université Paris Diderot
France
INSA de Toulouse
France

Keywords

formal methods, timed automata, [INFO.INFO-RB]Computer Science [cs]/Robotics [cs.RO], [INFO]Computer Science [cs], Robotics, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], transition systems, verification, semantics

[1] Tesnim Abdellatif, Saddek Bensalem, Jacques Combaz, Lavindra De Silva, and Fe´lix Ingrand. Rigorous design of robot software: A formal component-based approach. Robotics and Autonomous Systems, 60(12):1563-1578, 2012. [OpenAIRE]

[2] Rachid Alami, Raja Chatila, Sara Fleury, Malik Ghallab, and Fe´lix Ingrand. An architecture for autonomy. The International Journal of Robotics Research, 17(4):315-337, 1998. [OpenAIRE]

[3] Rajeev Alur and David Dill. A theory of timed automata. Theoretical computer science, 126(2):183-235, 1994.

[4] Ananda Basu, Bensalem Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, and Joseph Sifakis. Rigorous component-based system design using the bip framework. IEEE software, 28(3):41-48, 2011.

[5] Gerd Behrmann, Alexandre David, and Kim Larsen. A tutorial on uppaal. In Formal Methods for the Design of Real-Time Systems, pages 200-236. Springer, 2004.

[6] Albert Benveniste and Ge´rard Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE, 79:1270-1282, 1991.

[7] Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, Mamoun Filali, Hubert Garavel, Pierre Gaufillet, Frederic Lang, and Franc¸ois Vernadat. Fiacre: an intermediate language for model verification in the topcased environment. In European Congress on Embedded Real-Time Software and Systems, 2008.

[8] Se´bastien Bornot, Joseph Sifakis, and Stavros Tripakis. Modeling urgency in timed systems. In International Symposium on Compositionality: the significant difference, pages 103-129. Springer, 1998.

[9] Fre´de´ric Boussinot and Robert de Simone. The ESTEREL Language. In Proceeding of the IEEE, volume 79, pages 1293-1304, 1991.

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average

BIP!

Found an issue? Give us feedback

Average

Related to Research communities

Rural Digital Europe