An Algebraic Specification for the MPEG-2 Encoding Algorithm

The MPEG-2 encoding algorithm is a compression tool for moving pictures and associated audio, developed by the Moving Picture Experts Group (MPEG) and is designed to cover a wide range of requirements from ¿VHS quality¿ to¿HDTV¿. The compression methods used by MPEG-2 are considered to be asymmetrical in the meaning that the encoder is more complex than the decoder. This approach is new because MPEG does not specify the whole encoding process. In fact, the most important step of the encoding algorithm (namely the algorithms used to produce the motion vector) is not specified. Only some basic steps and the format of the compatible output are explicit specified, so that each encoder provider can create his own interpretation of the algorithm. This technique has the benefit that the decoders will remain compatible even as the encoders evolve. Due to its high acceptance and wide use, it is important to verify that the algorithm works as expected using formal methods, not only testing. To this end, we have used CafeOBJ, an executable algebraic specification language, to specify the algorithm and prove some desirable safety properties. More precisely, we specified the MPEG-2 encoding algorithm, considering the unspecified by MPEG steps as black boxes, as an Observational Transition System in CafeOBJ, and created a formal proof that for any input the output is as expected, thus proving that the algorithm works correctly.