A parallel version of the MPEG-2 encoding algorithm formally analyzed using algebraic specifications

Author

Ksystra, Katerina ; Stefaneas, Petros ; Ouranos, Iakovos ; Frangos, Panayiotis

Author_Institution

School of Electrical and Computer Engineering, National Technical University of Athens, Greece

fYear

2010

fDate

26-28 July 2010

Firstpage

35

Lastpage

38

Abstract

MPEG-2 is a wide used group of standards, established by the Moving Picture Experts Group (MPEG), for the digital compression of broadcast-quality full-motion video. Due to its high acceptance, it is very important to ensure that it behaves in a correct manner. To avoid vulnerability problems the MPEG-2 encoding algorithm has been already formally specified and verified for its correctness. In this paper, we propose the use of the OTS/CafeOBJ Method in order to prove that two MPEG-2 encoding algorithms for the same input produce the same output. Our approach is based on a simplified parallel version of the MPEG-2 encoder. Also, we have proved a mutual exclusion property for this parallel algorithm.

Keywords

Discrete cosine transforms; Encoding; Parallel algorithms; Prediction algorithms; Program processors; Quantization; Transform coding; CafeOBJ; MPEG-2 encoding algorithm; Observational Transition System; Parallel algorithm;

fLanguage

English

Publisher

ieee

Conference_Titel

Signal Processing and Multimedia Applications (SIGMAP), Proceedings of the 2010 International Conference on

Conference_Location

Athens

Type

conf

Filename

5742542