Using UPPAAL to analyze an MPEG 2 algorithm
M. Emilia Cambronero, Anders Peter Ravn, Valentín Valero · 2005
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. 1