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 → … |