Interface automata-based verification for Web applications

doi:10.3778/j.issn.1002-8331.2009.03.020

Computer Engineering and Applications ›› 2009, Vol. 45 ›› Issue (3): 70-73.DOI: 10.3778/j.issn.1002-8331.2009.03.020

• 研发、设计、测试 • Previous Articles Next Articles

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

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

谭亮,曾红卫

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

通讯作者: 谭亮

Abstract

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

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

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

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

[1]	ZHAO Yang, ZHANG Junhua. Multi-scale Feature Fusion Method for Spinal X-Ray Image Segmentation [J]. Computer Engineering and Applications, 2021, 57(8): 214-219.
[2]	LU Zhiliang, LIN Wei, ZENG Bi, LIU Ruixue. Real-Time Detection Method for Robot Target Grasping Area [J]. Computer Engineering and Applications, 2020, 56(19): 224-230.
[3]	DU Mengyao, WANG Zheng, LI Na, QIANG Yan. Dynamic Password Authentication Protocol for Wireless Body Area Network [J]. Computer Engineering and Applications, 2020, 56(14): 68-73.
[4]	ZHANG Xin1, ZOU Dexuan1, XIAO Peng1, YU Qiu2. Self-Adjusted Simplified Particle Swarm Optimization Algorithm and Its Application [J]. Computer Engineering and Applications, 2019, 55(8): 250-263.
[5]	WEI Qingjie1, LIU Shukun2. Method of Cross-Browser Compatibilities Testing for Web Application [J]. Computer Engineering and Applications, 2019, 55(5): 55-59.
[6]	YANG Wenxia, WANG Zheng, LI Na, MA Jianfen. Security Analysis and Improvement of Lightweight Mobile Payment Protocol LMPP [J]. Computer Engineering and Applications, 2019, 55(16): 88-93.
[7]	YOU Feng, ZHANG Yafeng, ZHAO Ruilian, MA Jinhui. Page cluster based research on Web application test method [J]. Computer Engineering and Applications, 2018, 54(5): 51-56.
[8]	ZHENG Bing1, LI Bin1, TIAN Lianfang1, DING Huanwen2, LI Liling1. Computer-aided design of personalized pedicle screw in spinal surgery [J]. Computer Engineering and Applications, 2018, 54(4): 218-224.
[9]	LI Qian1, WANG Zheng1, MA Jianfen1, LI Na2. Lightweight mobile payment protocol fairness analysis [J]. Computer Engineering and Applications, 2018, 54(19): 82-87.
[10]	XIA Zhijian, PENG Guojun, HU Hongfu. Detection of access control vulnerabilities in Web applications based on privilege verification graph [J]. Computer Engineering and Applications, 2018, 54(12): 63-68.
[11]	QIN Manman, WANG Zheng, WANG Li. Formal analysis and improvement of remote attestation protocol based on the SPIN [J]. Computer Engineering and Applications, 2017, 53(1): 34-38.
[12]	LV Jianghua1, LIU Zhifeng1, XU Yatao2, ZHOU Conghua1. Verification of correctness of attribute based access control [J]. Computer Engineering and Applications, 2016, 52(18): 98-103.
[13]	DENG Zhidan, YANG Haiyan, WU Ji. Test data generation and selection approach for Web application based on constraint-solving [J]. Computer Engineering and Applications, 2016, 52(18): 214-221.
[14]	XIA Chunrui1, WANG Rui1, LI Xiaojuan1, GUAN Yong1, ZHANG Jie2, WEI Hongxing3. Probabilistic model checking for path planning in dynamic environment [J]. Computer Engineering and Applications, 2016, 52(12): 5-11.
[15]	HUANG Yankai, ZHOU Yu, WEI Ou. Novel approach for attributed graph grammar response specification verification [J]. Computer Engineering and Applications, 2016, 52(12): 15-18.

Interface automata-based verification for Web applications

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

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics