Using UPPAAL to verify the MPEG-2 encoding algorithm

M.Emilia CambroneroAnders P. RavnValentín Valero

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. So, 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 bisimulation relation.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: