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:
Timing verification of an aerial video tracking system using UPPAAL
Timing verification of an aerial video tracking system using UPPAAL
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
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