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

doi:10.3778/j.issn.1002-8331.2009.03.020

计算机工程与应用 ›› 2009, Vol. 45 ›› Issue (3): 70-73.DOI: 10.3778/j.issn.1002-8331.2009.03.020

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

谭亮,曾红卫

上海大学计算机工程与科学学院，上海 200072

收稿日期:2008-07-21 修回日期:2008-10-24 出版日期:2009-01-21 发布日期:2009-01-21
通讯作者: 谭亮

Interface automata-based verification for Web applications

TAN Liang,ZENG Hong-wei

School of Computer Engineering and Science，Shanghai University，Shanghai 200072，China

Received:2008-07-21 Revised:2008-10-24 Online:2009-01-21 Published:2009-01-21
Contact: TAN Liang

摘要/Abstract

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

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

Abstract: 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.

Key words: Web application, interface automata, model checking, Spin

谭亮,曾红卫. 基于接口自动机的Web应用验证[J]. 计算机工程与应用, 2009, 45(3): 70-73.

TAN Liang,ZENG Hong-wei. Interface automata-based verification for Web applications[J]. Computer Engineering and Applications, 2009, 45(3): 70-73.

[1]	杜梦瑶，王峥，李娜，强彦. 适用于无线体域网的动态口令认证协议[J]. 计算机工程与应用, 2020, 56(14): 68-73.
[2]	韦庆杰1，刘淑坤2. 一种Web应用跨浏览器兼容性测试方法[J]. 计算机工程与应用, 2019, 55(5): 55-59.
[3]	杨文霞，王峥，李娜，马建芬. 轻量级移动支付协议LMPP的安全性分析与改进[J]. 计算机工程与应用, 2019, 55(16): 88-93.
[4]	尤枫，张雅峰，赵瑞莲，马金慧. 基于页面聚类的Web应用测试方法研究[J]. 计算机工程与应用, 2018, 54(5): 51-56.
[5]	夏志坚，彭国军，胡鸿富. 基于权限验证图的Web应用访问控制漏洞检测[J]. 计算机工程与应用, 2018, 54(12): 63-68.
[6]	秦嫚蔓，王峥，王莉. 基于SPIN的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.
[7]	邓志丹，杨海燕，吴际. 一种约束求解的Web应用测试数据生成与筛选方法[J]. 计算机工程与应用, 2016, 52(18): 214-221.
[8]	尤启房，杨晋吉. SIP协议的SPIN模型检测[J]. 计算机工程与应用, 2014, 50(13): 87-89.
[9]	吕威，黄志球，陈哲，阚双龙，魏欧. ESpin*：基于SPIN的Eclipse模型检测环境[J]. 计算机工程与应用, 2013, 49(7): 45-51.
[10]	董玲玲1，关永1，李晓娟1，施智平1，张杰2，华伟1. 用LTL模型检验的方法验证SpaceWire检错机制[J]. 计算机工程与应用, 2012, 48(22): 88-94.
[11]	缪力，谭志华，张大方. 基于SPIN的网络认证协议高效模型检测[J]. 计算机工程与应用, 2012, 48(21): 62-67.
[12]	薛疑1，叶晓俊2. 数据库活动监控工具的接口自动机模型[J]. 计算机工程与应用, 2012, 48(18): 110-114.
[13]	田野，曾红卫. 用模型检验产生约简测试集[J]. 计算机工程与应用, 2012, 48(17): 93-98.
[14]	李仁见，王昭飞. 命令式程序终止性验证方法综述[J]. 计算机工程与应用, 2011, 47(28): 1-6.
[15]	李莉1，翟征德2. 一种基于Web应用防火墙的主动安全加固方案[J]. 计算机工程与应用, 2011, 47(25): 104-106.

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

Interface automata-based verification for Web applications

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics