Formal verification and analysis of multimedia systems

Multimedia systems such as video-on-demand (VOD) servers are time critical systems. These systems have strict response times, which implies that a delayed response can have serious consequence. For instance, in the case of a VOD server, an immediate consequence of a delayed response time can be user dissatisfaction, what can ultimately lead to the end of a business based on this system. Therefore, analysis and verification of timing properties of multimedia systems is an important problem. To verify if time critical systems satisfy their time bounds, we discuss the use of formal methods tools, in the verification and analysis of multimedia systems. We have used Verus (a formal verification tool) to model and analyze the ALMADEM-VOD server, a component of a true video-on-demand system. The modeling of this server in Verus has provided great insight into its design and its dynamic behavior. Using the quantitative estimates provided by Verus, we have determined performance bounds to the server. These bounds have pointed out that the performance curve of the actual server was almost at the predicted upper bound (worst case) level. These curves have uncovered design inefficiencies. After optimizing the server, its performance has improved over 40%, showing how useful formal verification can be used successfully during the design of multimedia systems.