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

TL;DR

This paper models and analyzes the real-time latency of an aerial video tracking system using formal methods, providing bounds on latency and frame delay through model checking with Tina and Fiacre.

Contribution

It introduces formal models of an aerial video tracking system using Time Petri Nets and Fiacre, enabling precise latency analysis and delay bounds.

Findings

Computed worst and best-case end-to-end latency.

Established lower bounds on frame loss delay.

Demonstrated modeling benefits of Fiacre for buffering and data handling.

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.