MPEG-4可以有效地对视频数据进行压缩，但其结构复杂，直接进行应用开发的难度比较大。本文对MPEG-4视频压缩系统的建模及验证方面进行了研究，完成了基于UML的MPEG-4系统模型设计及验证，并实现了UML活动图到Petri网的转换器的设计。本文对系统建模的关键技术进行研究，其中包括面向对象的UML建模和形式化的Petri网建模。在掌握MPEG-4原理，熟悉视频处理的流程的基础上，利用UML对视频系统的关键模块（如DCT、量化、熵编码、运动估计和运动补偿等）进行建模。根据功能模块的特点，采用面向对象的设计方法从不同角度进行设计，主要包括用例图、类图、顺序图、活动图和状态图，完成视频压缩系统的UML建模。为实现系统模型的验证，在完成系统的UML建模后，进行UML活动图到Petri网的转换，利用Petri网对模型进行验证，并分析系统的并行性及死锁情况。本文提出转换思想和转换规则，利用JDOM接口编写转换器，实现UML活动图到Petri网的自动转换，完成对系统的分析和验证。该论文的工作对系统的形式化建模工作具有一定的参考价值。