| 一种验证Web应用设计的方法 |
| |
| 引用本文： | 曾红卫,缪淮扣.一种验证Web应用设计的方法[J].上海大学学报(自然科学版),2007,13(5):578-582. |
| |
| 作者姓名： | 曾红卫 缪淮扣 |
| |
| 作者单位： | 上海大学 计算机工程与科学学院，上海 200072 |
| |
| 基金项目： | 国家自然科学基金;国家重点实验室基金 |
| |
| 摘 要： | 提出一种表示Web应用的请求/响应导航关系的形式化行为模型，给出一种基于模型检查的Web应用设计的验证方法并描述了用时态逻辑CTL表示Web应用性质的方法.设计了一个检验方法可行性的原型框架，该原型嵌入自动化模型检查工具NuSMV，提供从UML设计模型到形式化模型的自动转换，在将用户输入的性质和形式化模型合并为NuSMV程序后，运行NuSMV进行自动化验证.
|
| 关 键 词： | Web应用 模型检查 时态逻辑 验证 |
| 文章编号： | 1007-2861（2007）05-0578-05 |
| 收稿时间： | 2007-04-13 |
| 修稿时间： | 2007年4月13日 |
An Approach to Verification of Web Application Design |
| |
| ZENG Hong-wei,MIAO Huai-kou.An Approach to Verification of Web Application Design[J].Journal of Shanghai University(Natural Science),2007,13(5):578-582. |
| |
| Authors: | ZENG Hong-wei MIAO Huai-kou |
| |
| Institution: | School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China |
| |
| 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. |
| |
| Keywords: | Web application verification model checking CTL |
| 本文献已被 维普 万方数据 等数据库收录！ |
| 点击此处可从《上海大学学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《上海大学学报(自然科学版)》下载免费的PDF全文 |
