PREMO : a case study in formal methods and multimedia system specification

SC24, the sub-committee of the International Organisation for Standardization responsible for the area of computer graphics and image processing, is in the process of completing work on a new standard for multimedia systems, called PREMO. For the first time in SC24, formal methods were employed during the development of the standard. The lessons learned from this exercise are interesting for two reasons. First, PREMO spans concerns ranging from the underlying object model through to issues related to media content. The broad scope of this work has presented challenges to the use of formal methods that have not been reported in other industrial applications. Second, the standards development process places restrictions on how formal methods can be applied. This paper describes the approaches that the PREMO specification group adopted to address the technical demands of the application area and, critically, where those approaches were found wanting. The lessons learned from the case study are discussed in the context of recent debates within the formal methods community on making formal methods relevant to software practitioners.