Large Integrating formal verification methods of quantitative real-time properties into a development environment for robot controllers

Muriel Jourdan 1
1 BIP - Biped Robot
Inria Grenoble - Rhône-Alpes
Abstract : In this paper we describe our experience with a development environment for robot controllers, which provides the user with formal verification functionalities. We study how to augment these functionalities by also allowing formal verification of quantitative real-time properties. Our approach is based on the timed extension of a synchronous language, named Timed-Argos, and on a symbolic model-checking tool named Kronos for the real-time temporal logic TCTL. We illustrate this approach by a real example taken from the area of autonomous vehicles, which poses some challenges on the applicability of the theory and finally, we discuss some possible solutions. This {\em large-scale} real application is also an opportunity to identify new research directions in the area of formal verification.
Type de document :
Rapport
RR-2540, INRIA. 1995
Liste complète des métadonnées

https://hal.inria.fr/inria-00074138
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:36:14
Dernière modification le : samedi 17 septembre 2016 - 01:35:46
Document(s) archivé(s) le : jeudi 24 mars 2011 - 12:13:40

Fichiers

Identifiants

  • HAL Id : inria-00074138, version 1

Collections

Citation

Muriel Jourdan. Large Integrating formal verification methods of quantitative real-time properties into a development environment for robot controllers. RR-2540, INRIA. 1995. 〈inria-00074138〉

Partager

Métriques

Consultations de la notice

86

Téléchargements de fichiers

82