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

An Approach to Verification of Web Application Design

作　　者：曾红卫[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《上海大学学报（自然科学版）》2007年第5期578-582,共5页Journal of Shanghai University:Natural Science Edition

基　　金：国家自然科学基金资助项目(60673115);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE05-13)

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

关 键 词：WEB应用 验证 模型检查 时态逻辑 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]