Tools and Benchmarks for Real-Time Systems

Verification challenge • Web page

2015-07-07T08:30:41+01:00

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

http://www.imitator.fr/FMTV15/

Statistics: Posted by etienneandre — Tue Jul 07, 2015

Verification challenge • Solving the 2015 FMTV challenge by response time analysis with MAST

2015-06-26T13:46:09+01:00

Title: Solving the 2015 FMTV Challenge by response time analysis with MAST

Authors: Julio L. Medina, Juan M. Rivas, J. Javier Gutiérrez, and Michael González Harbour (Departamento de Ingeniería Informática y Electrónica, Universidad de Cantabria, Santander, Spain)

Abstract: This paper reports solutions and recommendations regarding the design of the systems proposed in the 2015 edition of the Formal Methods and Timing Verification Challenge (FMTV). It uses the modelling formalism and the schedulability analysis techniques provided by the MAST suite of tools. The paper starts by clarifying the role of the data provided against the design intent. Then, for each of the challenges proposed, it discusses the adequacy of the analysis models used to represent the corresponding timing characteristics as well as the strengths and limitations of the underlying analysis approaches, and presents the results obtained. Finally, we report the effort it took to solve them and the lessons learned. The solutions are also provided in electronic form to facilitate their assessment by the community.

Attached paper:

FMTV15_Solution_MAST.pdf

Statistics: Posted by medinajl — Fri Jun 26, 2015

Verification challenge • Timing verification of an aerial video tracking system using UPPAAL

2015-06-26T13:42:54+01:00

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

Statistics: Posted by iceslj — Fri Jun 26, 2015

Verification challenge • Verification of two real-time systems using parametric timed automata

2015-06-26T13:39:11+01:00

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

Statistics: Posted by Sophie Quinton — Fri Jun 26, 2015

Verification challenge • Using CPAL to model and validate the timing behaviour of embedded systems

2015-06-26T13:32:42+01:00

Title: Using CPAL to model and validate the timing behaviour of embedded systems

Authors:
Sebastian Altmeyer, Nicolas Navet (University of Luxembourg, Luxembourg)
Loïc Fejoz (RealTime-at-Work, Villers-lès-Nancy, France)

Abstract: This work presents a solution to the Formal Methods for Timing Verification (FMTV) Challenge 2015 using CPAL. CPAL stands for the Cyber-Physical Action Language and is a novel language to model, simulate and verify cyber-physical systems as those described in the challenge. We believe that the complexity of the challenge mainly stems from the complex interactions of the tasks and processes composing the aerial video tracking system of the challenge. Using CPAL we have derived a complete and unambiguous description of the system that supports timing verification. The different sub-challenges were solved by timing-accurate simulation and/or schedulability analysis. Even though simulation does not provide firm guarantees on the worst-case behaviour, it helps the system designer solve scheduling problems and validate the solutions, where verification tools can not be applied directly due to the complexity of the model as in the 2015 FMTV challenge.

Paper:

FMTV15_Solution_CPAL.pdf

Slides:

CPAL_Slides.pdf

Statistics: Posted by SebastianAltmeyer — Fri Jun 26, 2015

Verification challenge • Latency analysis of an aerial video tracking system using Fiacre and Tina

2015-06-26T10:32:45+01:00

Title: Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina

Authors: Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan (CNRS/LAAS, Toulouse, France)

Abstract: We describe our experience with modeling a video tracking system used to detect and follow moving targets from an airplane. We provide a formal model that takes into account the real-time properties of the system and use it to compute the worst and best-case end to end latency. We also compute a lower bound on the delay between the loss of two frames. Our approach is based on the model-checking tool Tina, that provides state-space generation and model-checking algorithms for an extension of Time Petri Nets with data and priorities. We propose several models divided in two main categories: first Time Petri Net models, which are used to study the behavior of the system in the most basic way; then models based on the
Fiacre specification language, where we take benefit of richer data structures to directly model the buffering of video information and the use of an unbounded number of frame identifiers.

Attached paper:

FMTV15_Solution_Fiacre_Tina.pdf

Statistics: Posted by Sophie Quinton — Fri Jun 26, 2015

Verification challenge • The FMTV'15 Challenge

2015-06-23T16:13:26+01:00

About the FMTV Challenge
The purpose of the Formal Methods for Timing Verification (FMTV) challenge is to share ideas, experiences and solutions to a concrete timing verification problem issued from real industrial case studies. It also aims at promoting discussions, closer interactions, cross fertilization of ideas and synergies across the breadth of the real-time research community, as well as attracting industrial practitioners from different domains having a specific interest in timing verification.

The 2015 FMTV Challenge
The 2015 challenge is an industrial case study proposed by THALES, consisting of an aerial video tracking system used in intelligence, surveillance, reconnaissance, tactical and security applications. The challenge was presented to the research community at the FMTV’14 workshop (http://www.merge-project.eu/fmtv14-workshop). The system is characterized by strict and less strict constraints on timing. Two timing verification problems are proposed to the community. The first timing problem is related to a video frame processing chain in the aerial video tracking system and consists in calculating the timing latencies for the frame processing as well as the timing distance separating two successive frame losses. The second timing problem is related to a tracking and camera control subsystem of the aerial video tracking system and consists in calculating the timing latencies for the camera control function and optimizing the priorities assignment.

Attached description:

FMTV15_Challenge.pdf

Statistics: Posted by rafik — Tue Jun 23, 2015