Tools and Benchmarks for Real-Time Systems

Consolidated 2015 industrial challenge • Re: Challenge 2015 New Solution: Verification of an Aerial Video System

2017-05-20T20:20:42+01:00

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.

FMTV17_submitted.pdf

Statistics: Posted by youcheng.sun — Sat May 20, 2017

Consolidated 2015 industrial challenge • Challenge 2015 New Solution: Verification of an Aerial Video System

2017-05-19T17:01:16+01:00

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

Statistics: Posted by arne.hamann — Fri May 19, 2017

Consolidated 2015 industrial challenge • Industrial challenge 2015

2017-02-28T16:44:53+01:00

The industrial challenge of WATERS 2015 is proposed by Rafik Henia and Laurent Rioux from Thales Research & Technology France.

Details about the intention of the challenge can be found here: https://waters2017.inria.fr/challenge/.

A detailed description of the challenge can be found in the attached document:

WATERS2015_Industrial_Challenge_Thales.pdf

The corresponding challenge model in Papyrus (https://eclipse.org/papyrus/) is available here:

WATERS2015_Industrial_Challenge_Thales.zip

Statistics: Posted by rafik — Tue Feb 28, 2017