Latency analysis of an aerial video tracking system using Fiacre and Tina

The FMTV'15 challenge and its solutions presented at WATERS'15
Sophie Quinton
Site Admin
Posts: 46
Joined: Tue Apr 28, 2015
Location: Inria Grenoble - Rhône-Alpes, France

Latency analysis of an aerial video tracking system using Fiacre and Tina

Postby Sophie Quinton » Fri Jun 26, 2015

Title: Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina

Authors: Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan (CNRS/LAAS, Toulouse, France)

Abstract: We describe our experience with modeling a video tracking system used to detect and follow moving targets from an airplane. We provide a formal model that takes into account the real-time properties of the system and use it to compute the worst and best-case end to end latency. We also compute a lower bound on the delay between the loss of two frames. Our approach is based on the model-checking tool Tina, that provides state-space generation and model-checking algorithms for an extension of Time Petri Nets with data and priorities. We propose several models divided in two main categories: first Time Petri Net models, which are used to study the behavior of the system in the most basic way; then models based on the
Fiacre specification language, where we take benefit of richer data structures to directly model the buffering of video information and the use of an unbounded number of frame identifiers.

Attached paper:
(231.22 KiB) Downloaded 369 times
Sophie Quinton
INRIA Grenoble - Rhône-Alpes
655 Avenue de l'Europe - Montbonnot
38334 St Ismier Cedex - FRANCE
tel: +33 4 76 61 55 31

Return to “Verification challenge”

Who is online

Users browsing this forum: No registered users and 1 guest