基于接口自动机的Web应用验证

摘要：

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

关键词：Web应用、接口自动机、模型检验、Spin

所属期刊栏目：45

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金the National Natural Science Foundation of China under Grant 60673115

在线出版日期：2009-04-01（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：70-73