Web应用的验证与测试方法研究
| 摘要 | 第1-8页 |
| Abstract | 第8-12页 |
| 第1章 绪论 | 第12-19页 |
| ·Web应用的特性 | 第12-14页 |
| ·形式验证 | 第14页 |
| ·Web应用的形式验证 | 第14-16页 |
| ·测试 | 第16-17页 |
| ·Web应用的测试 | 第17页 |
| ·论文的主要研究内容 | 第17-19页 |
| 第2章 模型检验技术及其进展 | 第19-30页 |
| ·Kripke结构 | 第19-21页 |
| ·线性时态逻辑LTL | 第21-23页 |
| ·计算树逻辑CTL | 第23-24页 |
| ·模型检验优化技术 | 第24-27页 |
| ·模型检验工具 | 第27-28页 |
| ·模型检验与测试或定理证明的结合 | 第28页 |
| ·小结 | 第28-30页 |
| 第3章 Web应用导航行为的验证 | 第30-44页 |
| ·引言 | 第30-31页 |
| ·Web应用建模 | 第31-34页 |
| ·设计模型 | 第31-32页 |
| ·导航模型 | 第32-34页 |
| ·导航行为的一致性 | 第34-38页 |
| ·节点覆盖 | 第34-35页 |
| ·边覆盖 | 第35-36页 |
| ·边组合覆盖 | 第36-38页 |
| ·导航行为的安全策略 | 第38-40页 |
| ·导航行为验证原型 | 第40页 |
| ·SMV程序生成器 | 第40-42页 |
| ·性质检验 | 第42-43页 |
| ·小结 | 第43-44页 |
| 第4章 构件组合的抽象精化验证 | 第44-61页 |
| ·引言 | 第44-45页 |
| ·构件组合的形式建模 | 第45-47页 |
| ·抽象 | 第47-49页 |
| ·反例确认和精化 | 第49-54页 |
| ·抽象反例的有效性 | 第49-52页 |
| ·组合式反例确认 | 第52-54页 |
| ·抽象精化 | 第54-55页 |
| ·验证算法 | 第55-57页 |
| ·实例研究 | 第57-59页 |
| ·相关工作 | 第59-60页 |
| ·小结 | 第60-61页 |
| 第5章 构件组合的安全性验证 | 第61-70页 |
| ·引言 | 第61-62页 |
| ·自动机 | 第62-63页 |
| ·构件交互建模 | 第63-67页 |
| ·构件消息自动机 | 第63-64页 |
| ·构件组合 | 第64-67页 |
| ·可控性验证 | 第67-69页 |
| ·可控性(Controllability) | 第67页 |
| ·可控性的基本验证算法 | 第67-68页 |
| ·实例研究 | 第68-69页 |
| ·小结 | 第69-70页 |
| 第6章 基于模型检验的测试与优化 | 第70-82页 |
| ·引言 | 第70-71页 |
| ·使用模型检验器产生测试 | 第71-75页 |
| ·SMV的反例 | 第72-74页 |
| ·基于测试准则的性质生成 | 第74-75页 |
| ·测试优化 | 第75-81页 |
| ·测试树(Test-tree) | 第76-77页 |
| ·测试树生成 | 第77-81页 |
| ·小结 | 第81-82页 |
| 第7章 基于模型检验的Web应用测试 | 第82-101页 |
| ·引言 | 第82-83页 |
| ·相关工作 | 第83-85页 |
| ·导航行为的测试 | 第85-91页 |
| ·从WA_D到WA_N的转换 | 第86-87页 |
| ·导航性质的生成 | 第87-89页 |
| ·实例研究 | 第89-91页 |
| ·基于数据流的Web应用测试 | 第91-100页 |
| ·对象状态机OSM | 第92-93页 |
| ·对象流图OFG | 第93-95页 |
| ·标记OFG | 第95-96页 |
| ·数据流陷阱性质的生成 | 第96-100页 |
| ·小结 | 第100-101页 |
| 第8章 结束语 | 第101-104页 |
| ·主要贡献 | 第101-102页 |
| ·将来的工作 | 第102-104页 |
| 参考文献 | 第104-111页 |
| 附录1 SGRS导航模型的SMV程序 | 第111-119页 |
| 附录2 SMV输出的反例 | 第119-128页 |
| 作者在攻读博士学位期间发表的论文与译著 | 第128-129页 |
| 作者在攻读博士学位期间参与的科研项目 | 第129-130页 |
| 致谢 | 第130页 |
