随着Internet的迅速发展和应用，WEB应用已经渗透到国计民生的各个领域。相比一般传统软件，WEB应用具有更高的质量需求。WEB应用本身的高复杂性使的对其验证、测试都相当困难，基于模型检查的Web应用验证方法是保证WEB应用质量的方法之一。　　 目前已有众多的模型检查方法和多种模型结构，Petri网是其中一种重要的模型描述工具，Petri网能够自然地描述并发、同步、资源竞争等系统特性，易于描述Web服务的动态行为。故基于Petri网的Web服务模型适于验证Web应用的运行过程。　　 本文对Web服务应用的验证模型构建进行研究，通过分析WEB应用描述语言SCXML，基于Petri网模型形式对系统模型进行模型检查。　　 本文主要工作如下：　　 1．分析了WEB应用建模语言SCXML，根据WEB应用的特征和SCXML语言具有的并发性、控制等性质，分析了WEB应用的行为、性质等。　　 2．通过对SCXML中元素属性的分析，实现了将现有的Web服务应用描述语言SCXML转化为模型检测器可以接受的模型------基于对扩展的Petri网的形式描述，达到SCXML到扩展Petri网的转化，使SCXML描述的并发、同步、资源竞争等WEB系统特性能够在扩展Petri网结构模型上得以体现，为Web服务转换性质的分析与验证提供有力的支持。　　 3．详细探讨了基于Petri网的模型检查算法，并引入on-the-fly技术进行Petri网的模型检查，同时对on-the-fly算法进行优化，以此来减缓状态空间爆炸的问题，使存储规范Petri网模型和待验证Petri网模型的交Petri网模型所占用的空间减少，从而很好地缓解内存不足的问题。　　 4．在提出了基于on-the-fly的Petri网的模型检查算法的基础上，用JAVA语言对算法进行了实现，并通过实例测试基于on-the-fly算法的Petri网模型检查算法的正确性。