Challenge 2015 New Solution: Verification of an Aerial Video System

[arne.hamann]

Authors: Youcheng Sun, Étienne André and Giuseppe Lipari

[youcheng.sun]

In this paper we propose solutions to the consolidated version of the WATERS 2015 industrial challenge of a distributed video processing system using the formalism of Parametric Timed Automata (PTA). The first challenge is harder because of the very large number of states to be analyzed, so we only provide upper bounds. The second challenge consists of a real-time scheduling problem for which we provide exact solutions by using a scheduling analysis based on the critical instant, and a PTA model.

Furthermore, regarding the second challenge, we provide formal analysis for the frequency of possible temporal violations in the system, by applying the latest results from the so called weakly hard real-time schedulability analysis. This improvement contributes the major extension of this paper with respect to our solutions to the previous version of the challenge.