随着网络及其技术的迅速发展，WEB应用被广泛应用于国计民生的各个领域。与此同时，随着需求量与应用领域的不断扩大，对WEB应用的正确性、有效性和安全性等方面都提出了越来越高的要求。为最大限度减少WEB应用的缺陷，保证和提高WEB应用的质量，如何对WEB应用进行有效的验证、测试逐渐成为人们研究所面临的主要问题。　　 模型检查是对有穷状态系统的一种形式化验证方法，它基于状态搜索的基本思想。WEB应用的复杂性、动态性、异构性、组成成分和链接的多样性等使得直接对WEB应用进行验证相当困难。对基于建模语言State Chart XML( SCXML)的WEB应用进行模型检查的研究和应用是本文讨论的重点。为避免WEB应用模型检查中内存不足和状态爆炸等问题，本文把“On-the-Fly”技术引入到针对WEB应用的模型检查中。本文的主要工作有：　　 1．研究了WEB应用建模语言SCXML。根据WEB应用的特征，用SCXML对抽象出来的WEB应用的关键的行为、性质进行表示。　　 2．在深入分析SCXML的语法和语义的基础上，在此语言的子集上，研究并提出了一个由SCXML向Büchi自动机转换的算法，同时引用并实现了一个有效的算法用于从LTL公式向Büchi自动机的转换。　　 3．基于模型检查的特性，针对WEB应用的正确、安全和有效性等性质进行验证，采用模型检查的“On-the-Fly”算法，实现了“On-the-Fly”的模型检查系统，从而实现对WEB应用进行有效的验证，并用C＃语言实现了整个系统。　　 4．运用基于WEB应用的“On-the-Fly”模型检查方法对实例进行了验证测试，在验证WEB应用不满足某些性质时给出反例，并对验证结果进行了分析与讨论，并对今后的研究工作进行了展望。　　 基于以上工作，对建模后能用SCXML表示的WEB应用可运用本文的算法进行模型检查，扩大了模型检查在WEB应用中的研究领域。