Using UPPAAL to Analyze an MPEG-2 Algorithm

M. Emilia Cambronero; Anders Peter Ravn; Valentin Valero

Using UPPAAL to Analyze an MPEG-2 Algorithm

M. Emilia Cambronero, Anders Peter Ravn, Valentin Valero

Institut for Datalogi

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

Abstract

The performance of a parallel algorithm for an MPEG-2 encoding is analyzed using timed automata models in the UppAal tool. We have constructed both a sequential model of MPEG-2, and a parallel model of MPEG-2 and then, a comparison of the results obtained for both models is made. We show how a model checking tool for timed automata is used to find exact bounds on the performance. Finally, we outline a correctness proof for the parallelization of the algoritm using an untimed bisiumulation relation.

Originalsprog	Engelsk
Titel	Proceedings of the VII Workshop Brasileiro de Tempo Real
Antal sider	6
Publikationsdato	2005
Sider	73-82
Status	Udgivet - 2005
Begivenhed	VII Workshop Brasileiro de Tempo Real - Varighed: 19 maj 2010 → …

Konference

Konference	VII Workshop Brasileiro de Tempo Real
Periode	19/05/2010 → …

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Citationsformater

@inproceedings{764faba031c611db8de7000ea68e967b,

title = "Using UPPAAL to Analyze an MPEG-2 Algorithm",

abstract = "The performance of a parallel algorithm for an MPEG-2 encoding is analyzed using timed automata models in the UppAal tool. We have constructed both a sequential model of MPEG-2, and a parallel model of MPEG-2 and then, a comparison of the results obtained for both models is made. We show how a model checking tool for timed automata is used to find exact bounds on the performance. Finally, we outline a correctness proof for the parallelization of the algoritm using an untimed bisiumulation relation.",

keywords = "parallel algorithm, performance estimation, model checking",

author = "Cambronero, {M. Emilia} and Ravn, {Anders Peter} and Valentin Valero",

year = "2005",

language = "English",

pages = "73--82",

booktitle = "Proceedings of the VII Workshop Brasileiro de Tempo Real",

note = "VII Workshop Brasileiro de Tempo Real ; Conference date: 19-05-2010",

}

TY - GEN

T1 - Using UPPAAL to Analyze an MPEG-2 Algorithm

AU - Cambronero, M. Emilia

AU - Ravn, Anders Peter

AU - Valero, Valentin

PY - 2005

Y1 - 2005

N2 - The performance of a parallel algorithm for an MPEG-2 encoding is analyzed using timed automata models in the UppAal tool. We have constructed both a sequential model of MPEG-2, and a parallel model of MPEG-2 and then, a comparison of the results obtained for both models is made. We show how a model checking tool for timed automata is used to find exact bounds on the performance. Finally, we outline a correctness proof for the parallelization of the algoritm using an untimed bisiumulation relation.

AB - The performance of a parallel algorithm for an MPEG-2 encoding is analyzed using timed automata models in the UppAal tool. We have constructed both a sequential model of MPEG-2, and a parallel model of MPEG-2 and then, a comparison of the results obtained for both models is made. We show how a model checking tool for timed automata is used to find exact bounds on the performance. Finally, we outline a correctness proof for the parallelization of the algoritm using an untimed bisiumulation relation.

KW - parallel algorithm

KW - performance estimation

KW - model checking

M3 - Article in proceeding

SP - 73

EP - 82

BT - Proceedings of the VII Workshop Brasileiro de Tempo Real

T2 - VII Workshop Brasileiro de Tempo Real

Y2 - 19 May 2010

ER -

Using UPPAAL to Analyze an MPEG-2 Algorithm

Abstract

Konference

AUB Link

Fingeraftryk

Citationsformater