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

作者：谭亮 曾红卫web应用接口自动机模型检验spin

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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社