一种验证Web应用设计的方法

上海大学学报(自然科学版)

一种验证Web应用设计的方法

曾红卫，缪淮扣

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

收稿日期:2007-04-13 修回日期:1900-01-01 出版日期:2007-10-20 发布日期:2007-10-20

An Approach to Verification of Web Application Design

ZENG Hong-wei，MIAO Huai-kou

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

Received:2007-04-13 Revised:1900-01-01 Online:2007-10-20 Published:2007-10-20

摘要/Abstract

摘要： 提出一种表示Web应用的请求/响应导航关系的形式化行为模型，给出一种基于模型检查的Web应用设计的验证方法并描述了用时态逻辑CTL表示Web应用性质的方法.设计了一个检验方法可行性的原型框架，该原型嵌入自动化模型检查工具NuSMV，提供从UML设计模型到形式化模型的自动转换，在将用户输入的性质和形式化模型合并为NuSMV程序后，运行NuSMV进行自动化验证.

关键词: Web应用, 模型检查, 时态逻辑, 验证

Abstract: A formal model representing the navigation behavior of a Web application as a Kripke structure is proposed, and an approach that applies the model checking technique to verify Web application design is presented. A collection of properties that a Web application should satisfy is specified in CTL formulas, and then model checked against the formal model by using model checker NuSMV. A prototype that embeds the NuSMV verifier automatically parses the XMI output of UML tool and builds the NuSMV program.

Key words: CTL, model checking, verification, Web application

曾红卫;缪淮扣. 一种验证Web应用设计的方法[J]. 上海大学学报(自然科学版).

ZENG Hong-wei;MIAO Huai-kou. An Approach to Verification of Web Application Design[J]. Journal of Shanghai University（Natural Science Edition）.

[1]	晏霞敏，曾红卫，刘攀，贺斌. 一种Web应用测试生成与约简方法[J]. 上海大学学报(自然科学版), 2012, 18(2): 163-169.
[2]	戴雨婷，缪淮扣，梅佳，高洪皓. 基于LSC模型检验的性质抽取[J]. 上海大学学报(自然科学版), 2012, 18(2): 156-162.
[3]	黄龙1,2,缪淮扣1,2,王皙1,2,郭亮1,2. 基于场景的形式化测试模型生成方法[J]. 上海大学学报(自然科学版), 2011, 17(5): 595-599.
[4]	胡越黎，经文怡，宣祥光. 基于NanoSim-VCS的芯片级混合信号验证[J]. 上海大学学报(自然科学版), 2009, 15(1): 42-46.
[5]	杨洪斌;韩霞;吴悦. 验证平台中的可重用监视器[J]. 上海大学学报(自然科学版), 2007, 13(5): 560-565 .