Title :
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
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;
Conference_Titel :
Signal Processing and Multimedia Applications (SIGMAP), Proceedings of the 2010 International Conference on
Conference_Location :
Athens
