Web应用的快速发展及其一些异于传统程序的特点使Web应用的验证面临了新的挑战。使用接口自动机对Web应用的构件和构件组合进行行为建模，设计了接口自动机到模型检验器Spin程序的转换算法，然后利用Spin检验Web应用的性质，通过一个简单的网上银行示例说明了整个验证过程。