Timing verification of an aerial video tracking system using UPPAAL

The FMTV'15 challenge and its solutions presented at WATERS'15
User avatar
iceslj
Posts: 6
Joined: Wed Jul 01, 2015
Location: Verimag @ Grenoble

Timing verification of an aerial video tracking system using UPPAAL

Postby iceslj » Fri Jun 26, 2015

Title: Timing Verification of an Aerial Video Tracking System Using UPPAAL

Authors:
Lijun Shan (College of Computer Science, Northwestern Polytechnical University, Xi'an, China)
Susanne Graf (Verimag/CNRS,Gières, France)

Abstract: This paper presents two different approaches for verifying the timing properties of the industrial use cases proposed as two challenges by WATERS’2015. The system under study is an aerial video system which contains two parts, a multiprocessor system and a uni-processor multitasking system. A timed automata model is constructed for each subsystem with the model checker UPPAAL. The symbolic model checking and statistical model checking functions of UPPAAL are applied to verify the models. Each of the models is modular, reusable and extensible, and can act as a general modeling framework for analyzing a type of systems.

Keywords: Real-time systems; verification; model checking

Attached paper:
FMTV15_Solution_UPPAAL.pdf
(300.01 KiB) Downloaded 410 times
Lijun SHAN
E-mail: lijun.shan@imag.fr.
VERIMAG
2, Avenue de Vignate
Centre Equation
F - 38610 GRENOBLE - Gières, FRANCE
Phone : (33) 04.56.52.03.76

Return to “Verification challenge”

Who is online

Users browsing this forum: No registered users and 1 guest