HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:36:14 PM
Last modification on : Friday, February 4, 2022 - 3:23:52 AM
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

34

Files downloads

86