Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074138
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:36:14 PM
Last modification on : Thursday, February 11, 2021 - 2:40:03 PM
Long-term archiving on: : Thursday, March 24, 2011 - 12:13:40 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

116

Files downloads

185