Verification of two real-time systems using parametric timed automata

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
Contact:

Verification of two real-time systems using parametric timed automata

Postby Sophie Quinton » Fri Jun 26, 2015

Title: Verification of Two Real-Time Systems Using Parametric Timed Automata

Authors:
Youcheng Sun (Scuola Superiore Sant’Anna, Pisa, Italy)
Étienne André (LIPN, Université Paris 13, France)
Giuseppe Lipari (University of Lille, France)

Abstract: In this paper we propose solutions to the FMTV 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 analysed, 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.

Attached paper:
FMTV15_Solution_Parametric_Timed_Automata.pdf
(249.77 KiB) Downloaded 355 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
https://team.inria.fr/spades/quinton/

etienneandre
Posts: 1
Joined: Tue Jul 07, 2015
Location: Université Paris 13
Contact:

Web page

Postby etienneandre » Tue Jul 07, 2015

Our solution (IMITATOR source and binary), models and results is available at:

http://www.imitator.fr/FMTV15/
Étienne André
Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France


Return to “Verification challenge”

Who is online

Users browsing this forum: No registered users and 1 guest