Web应用的快速发展及其一些异于传统程序的特点使Web应用的验证面临了新的挑战。使用接口自动机对Web应用的构件和构件组合进行行为建模,设计了接口自动机到模型检验器Spin程序的转换算法,然后利用Spin检验Web应用的性质,通过一个简单的网上银行示例说明了整个验证过程。
The rapid development and some new characteristics of Web applications give rise to new challenges for the verification of Web applications.We model components and their combination of Web applications through interface automata,design an algorithm converting interface automata to Promela,and then verify Web applications by model checker Spin.A simple Web bank example is used to illustrate the whole verification process.