学位论文 > 优秀研究生学位论文题录展示

Web应用的验证与测试方法研究

作　者: 曾红卫
导　师: 缪淮扣
学　校: 上海大学
专　业: 控制理论与控制工程
关键词: Web应用形式验证基于模型检验的测试构件组合反例引导的抽象精化
分类号: TP311.52
类　型: 博士论文
年　份: 2008年
下　载: 443次
引　用: 6次
阅　读: 论文下载

内容摘要

Internet的普及以及分布式计算、基于构件的开发和Web Services等技术的迅速发展和应用使Web应用渗透到国计民生的各个领域。Web应用的质量将直接影响人们的生活和工作。验证与测试是保证软件质量的最基本和最重要的手段。然而,Web应用是一种具有多层结构的分布式系统,异构性、动态性、连接的多样性和控制流程的可变性等特性给Web应用的验证和测试带来了严峻的挑战,必须改进传统的或提出新的验证和测试方法以适应Web应用的新特性。模型检验是一种自动化的、基于模型的性质验证方法,广泛应用于有限状态系统的自动验证。它通过有效地搜索有限状态模型的整个状态空间判定性质是否得到满足,在系统不满足性质时提供的反例可以用于诊断系统的错误。测试的目的在于发现系统的实际行为与预期行为是否存在不一致。传统的手工测试是低效的、易出错的、盲目的和不可再生的,并且受制于测试工程师的创造力。应用模型检验技术实现测试的自动化是当前的一个研究热点。使用模型检验自动生成测试用例的关键在于构造能使模型检验器输出反例的陷阱性质,然后从反例构造测试用例。论文以模型检验器SMV为形式验证工具,主要研究在模型检验的统一框架下Web应用的形式验证和功能测试方法。Web应用客户端的功能主要体现在它的导航行为,Web应用的质量的一个重要方面是导航行为的一致性和安全性。论文给出了用对象联系图描述导航相关对象以及对象间联系的结构建模方法,提出了用Kripke结构进行导航的行为建模的形式化方法并分别从验证角度和测试角度定义了导航行为与对象联系图之间的一致性关系。在此基础上,提出了基于模型检验的导航行为的一致性验证方法和一致性测试方法,设计了从Kripke结构到SMV程序的转换算法,并分别实现了导航行为的验证原型与测试原型。此外,根据常用的导航安全策略,给出了导航行为的安全性验证方法。Web应用服务器通过构件的组合提供业务逻辑和应用服务,形式验证构件组合的行为是保证Web应用质量的一个有效手段。针对构件组合验证的状态爆炸问题,论文结合组合推理和反例引导的抽象精化思想,提出了组合式的抽象精化方法并设计了相应的检验算法,使构件组合的模型检验转化为各成分构件的局部抽象精化。提出并证明了组合确认定理,使构件组合上的反例确认转化为各构件上的反例投影确认。构件组合的一个验证问题是组合行为是否隐含了不安全的行为?论文提出了一种新的描述构件交互行为的模型:构件消息自动机。基于监控理论的可控性概念,设计了一个验证构件组合行为安全性质的算法。对象(网页或构件)是Web应用导航和构件组合的基础。结合模型检验技术和数据流测试准则,论文提出了Web应用对象的自动测试生成方法。在对象的源代码不可用的情况下,对象的动态状态行为用对象状态机建模,然后被转换为描述控制流和数据流信息的对象流图。提出了基于数据流测试准则的陷阱性质生成方法,通过在对象流图上模型检验这些陷阱性质自动产生对象的数据流测试用例,实现了一个基于模型检验的对象数据流测试原型。用模型检验自动产生测试的一个缺陷是模型检验往往会产生大量冗余的反例。为此,论文提出了一种on-the-fly测试优化方法并设计了优化算法。当模型检验产生一个新反例时,一方面用新反例检测未检验的性质以消除冗余性质,另一方面比较现有测试集以消除冗余测试。

全文目录

摘要  6-8
Abstract  8-12
第1章绪论  12-19
  1.1 Web应用的特性  12-14
  1.2 形式验证  14
  1.3 Web应用的形式验证  14-16
  1.4 测试  16-17
  1.5 Web应用的测试  17
  1.6 论文的主要研究内容  17-19
第2章模型检验技术及其进展  19-30
  2.1 Kripke结构  19-21
  2.2 线性时态逻辑LTL  21-23
  2.3 计算树逻辑CTL  23-24
  2.4 模型检验优化技术  24-27
  2.5 模型检验工具  27-28
  2.6 模型检验与测试或定理证明的结合  28
  2.7 小结  28-30
第3章 Web应用导航行为的验证  30-44
  3.1 引言  30-31
  3.2 Web应用建模  31-34
    3.2.1 设计模型  31-32
    3.2.2 导航模型  32-34
  3.3 导航行为的一致性  34-38
    3.3.1 节点覆盖  34-35
    3.3.2 边覆盖  35-36
    3.3.3 边组合覆盖  36-38
  3.4 导航行为的安全策略  38-40
  3.5 导航行为验证原型  40
  3.6 SMV程序生成器  40-42
  3.7 性质检验  42-43
  3.8 小结  43-44
第4章构件组合的抽象精化验证  44-61
  4.1 引言  44-45
  4.2 构件组合的形式建模  45-47
  4.3 抽象  47-49
  4.4 反例确认和精化  49-54
    4.4.1 抽象反例的有效性  49-52
    4.4.2 组合式反例确认  52-54
  4.5 抽象精化  54-55
  4.6 验证算法  55-57
  4.7 实例研究  57-59
  4.8 相关工作  59-60
  4.9 小结  60-61
第5章构件组合的安全性验证  61-70
  5.1 引言  61-62
  5.2 自动机  62-63
  5.3 构件交互建模  63-67
    5.3.1 构件消息自动机  63-64
    5.3.2 构件组合  64-67
  5.4 可控性验证  67-69
    5.4.1 可控性(Controllability)  67
    5.4.2 可控性的基本验证算法  67-68
    5.4.3 实例研究  68-69
  5.5 小结  69-70
第6章基于模型检验的测试与优化  70-82
  6.1 引言  70-71
  6.2 使用模型检验器产生测试  71-75
    6.2.1 SMV的反例  72-74
    6.2.2 基于测试准则的性质生成  74-75
  6.3 测试优化  75-81
    6.3.1 测试树(Test-tree)  76-77
    6.3.2 测试树生成  77-81
  6.4 小结  81-82
第7章基于模型检验的Web应用测试  82-101
  7.1 引言  82-83
  7.2 相关工作  83-85
  7.3 导航行为的测试  85-91
    7.3.1 从WA_D到WA_N的转换  86-87
    7.3.2 导航性质的生成  87-89
    7.3.3 实例研究  89-91
  7.4 基于数据流的Web应用测试  91-100
    7.4.1 对象状态机OSM  92-93
    7.4.2 对象流图OFG  93-95
    7.4.3 标记OFG  95-96
    7.4.4 数据流陷阱性质的生成  96-100
  7.5 小结  100-101
第8章结束语  101-104
  8.1 主要贡献  101-102
  8.2 将来的工作  102-104
参考文献  104-111
附录1 SGRS导航模型的SMV程序  111-119
附录2 SMV输出的反例  119-128
作者在攻读博士学位期间发表的论文与译著  128-129
作者在攻读博士学位期间参与的科研项目  129-130
致谢  130

相似论文

高校科研项目管理系统设计与实现,TP311.52
基于Web日志的入侵检测系统设计与实现,TP393.08
基于SOA的学籍管理系统的研究与实现,TP311.52
基于WEB的多角色协同工作的软件配置项管理系统,TP311.52
一种高安全的Web应用访问控制模型的研究,TP393.08
基于WCF和Silverlight的Web应用框架技术研究,TP393.09
基于事件的跨平台移动应用开发框架设计与实现,TP311.52
移动互联网中基于会话的Web负载测试研究,TN929.5
互联网支付企业WEB应用安全防护系统测试,TP393.08
苏家屯铁路货运调度中心计算机管理系统,TP311.52
Ajax技术在“数字校园”中的应用研究,TP311.52
面向自适应中间件的语义构件动态组合研究与应用,TP311.52
WEB快速开发框架的设计与实现,TP311.52
基于EOS芯片MAC模块的EDA验证,TN402
基于ASP.NET AJAX技术的国家精品课程网站设计与实现,TP393.092
网站内容管理在Ruby on Rails下的架构研究,TP393.092
Blog系统的设计与实现,TP393.092
乐家卫浴公司人力资源管理系统设计与实现,TP311.52
RIA及其在网络购物系统中的应用,TP311.52
糖尿病信息管理系统的开发与应用,TP311.52
基于MDA的Web应用系统开发框架的设计与实现,TP311.52