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

基于时间属性序列图的运行时验证技术研究

作　者: 辜剑
导　师: 叶俊民
学　校: 华中师范大学
专　业: 计算机软件与理论
关键词: 时间属性序列图 时间自动机 监控器 运行时验证
分类号: TP306
类　型: 硕士论文
年　份: 2014年
下　载: 5次
引　用: 0次
阅　读: 论文下载
 

内容摘要


随着信息技术的发展,计算机技术已经融入了现代社会各个领域,得到极其广泛的应用。然而在这样的背景下,计算机系统的异常可能会造成灾难性后果。测试和仿真通常被用来保障这类安全关键系统的可靠性,但是这类方法针对的是实际运行前的系统,只能检测到系统的错误,而不能证明系统的正确。模型验证是完备的,但是它针对的是系统的抽象模型,难以证明系统的抽象模型和实际系统的等价性,同时这种方法需要遍历系统的所有执行路径,对于复杂系统来说,容易产生组合爆炸问题。与传统的测试和模型验证技术不同,运行时验证针对的是正在运行的实际系统。运行时验证一般采用时态逻辑来描述要验证的需求规约,并根据需求规约构造监控器。利用UML序列图来描述要验证的需求规约,克服了时态逻辑等形式化方法使用复杂的问题,使得普通的软件工程师也能方便正确的描述要验证的需求规约或性质。研究基于时间属性序列图(TPSD, Timed Property Sequence Diagram)自动生成监控器来进行运行时验证就显得十分有意义。本文提出了基于UML2.0时间属性序列图的运行时验证方法,其具体思想是使用时间属性序列图来描述要验证的需求规约,然后为序列图中的每个对象构造时间对象自动机,将整个序列图转换为时间自动机网络,以构造出运行时验证中所需的监控器,监控器监控目标系统的执行轨迹,判断目标系统的当前执行是否满足需求规约。本文先给出了满足本文验证需求的时间属性序列图形式化定义,接着提出了时间对象自动机及其形式化定义,然后提出了基于时间属性序列图的运行时验证方法的基本原理,进而提出了将时间属性序列图转化为时间自动机网络来构造预测监控器的算法。在此基础上,本文利用上述原理构造了一个基于时间属性序列图的运行时验证工具TPSD_monitor,构造了一个列控系统CTCS-2向CTCS-3级间切换仿真程序作为要验证的目标系统,利用该工具对构造的目标系统进行运行时验证,说明了本文中方法对安全关键系统进行运行时验证的可行性。进而进行了性能对比试验,实验表明,本文的监控器构造方法所产生的监控器运行开销较小,且能在一定程度上缓解监控器生成过程中的组合爆炸问题。

全文目录


中文摘要  5-6
Abstract  6-12
第一章 绪论  12-19
  1.1 研究动因  12-13
  1.2 当前的研究现状  13-17
    1.2.1 国外的研究现状  14-15
    1.2.2 国内的研究现状  15-16
    1.2.3 存在的问题  16-17
  1.3 本文的研究目标与工作  17
  1.4 论文的组织结构  17-19
第二章 研究基础  19-30
  2.1 运行时验证相关理论  19-21
  2.2 UML序列图相关理论  21-25
    2.2.1 序列图的基本组成  21-22
    2.2.2 UML2.0序列图的新特性  22-23
    2.2.3 序列图的形式化定义  23-25
  2.3 时间自动机相关理论  25-26
  2.4 面向方面编程相关理论  26-29
  2.5 本章小结  29-30
第三章 基于UML2.0时间属性序列图的运行时验证方法  30-44
  3.1 基于时间属性序列图的运行时验证原理  30-33
    3.1.1 时间属性序列图  30-31
    3.1.2 基于时间属性序列图的运行时验证原理  31-33
  3.2 基于UML2.0时间属性序列图的监控器构造算法  33-43
  3.3 相关工作对比  43
  3.4 本章小结  43-44
第四章 实验结果及分析  44-56
  4.1 功能性试验  44-53
    4.1.1 实验样例设计  45-46
    4.1.2 需求规约建模  46-48
    4.1.3 构造运行时监控器  48-50
    4.1.4 代码插装  50-51
    4.1.5 运行时监控  51-52
    4.1.6 实验结果  52-53
  4.2 性能对比试验  53-54
  4.3 相关工作对比  54-55
  4.4 本章小结  55-56
第五章 总结和展望  56-57
  5.1 本文工作的总结  56
  5.2 进一步的研究工作  56-57
参考文献  57-63
校期间参加的科研项目和发表的论文  63-64
致谢  64

相似论文

  1. 基于Moore自动机的机器博弈系统建模与研究,TP18
  2. 基于硬件虚拟化的文件保护系统的研究,TP309
  3. 基于应用监控理论的信息系统安全监控和风险评估,TP393.08
  4. 基于时间自动机模型的CBTC系统安全计算机平台的形式化验证,U284.48
  5. 高速列车车厢压力监控器及其实验台的研制,U270.14
  6. 基于时间自动机的模型验证技术,TP301.1
  7. 软件行为运行时验证研究,TP311.52
  8. 虚拟机监控器内存管理机制研究与实现,TP391.9
  9. 基于MDE的UML模型到形式化模型的转换方法研究,TP311.52
  10. 虚拟机监控器体系结构研究,TP277
  11. IF对实时软件设计图形模型的验证,TP311.52
  12. 基于运行时验证的列控系统形式分析,TP273
  13. 分布式实时系统调度分析工具的改进研究,TP311.52
  14. 基于时间自动机的CTCS-3级列控车载设备建模与验证,U284.48
  15. 基于XYZ/ADL的Web服务组合验证研究,TP393.09
  16. 基于三值语义的软件运行时验证方法,TP311.52
  17. SMART-VMM：基于VT-x的虚拟机监控器设计与实现,TP302
  18. 基于运行时验证的AOP程序检测框架研究,TP311.52
  19. 对时间输入/输出自动机有效地进行一致性测试,TP311.5
  20. 基于时间自动机的模型验证理论及应用研究,TP301.1
  21. 基于uClinux的新型变压器监控器设计及应用,TM571

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 一般性问题 > 调整、测试、校验
© 2012 www.xueweilunwen.com