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

基于时间自动机的模型验证技术

作　者: 程永江
导　师: 周清雷
学　校: 郑州大学
专　业: 计算机软件与理论
关键词: 实时系统 模型验证 时间自动机 二元决策图 验证工具
分类号: TP301.1
类　型: 硕士论文
年　份: 2009年
下　载: 74次
引　用: 1次
阅　读: 论文下载
 

内容摘要


随着计算机科学的发展,工业界越来越重视系统的正确性和可靠性,这样使得形式化的模型验证方法得到了广泛地应用。通过可达性分析,模型检测可以完成对实时系统的安全性和活性的验证。它的思想是搜索描述系统行为的转换系统,然后分析可达状态集合,从而确定系统是否满足规格说明。时间自动机是包含时间约束的有限状态转换系统,它是使用最为广泛的形式化验证方法之一。在理论研究部分,首先分析了时间自动机的概念,然后给出了时间自动机的一些扩展形式。实时系统中的事件能否发生对应着时间自动机某个状态从初始状态开始能否可达,因此模型验证主要任务是状态可达性分析。验证需要采用了一些符号化的方法来描述状态,文中首先对时钟区域和时钟带两种方法进行了分析,然后介绍了可达性分析的两种主要的方法。我们重点介绍了基于二元决策图的模型验证方法,而使用它的前提是在时间自动机的整数语义下。详细地解释了如何把整数语义下的状态和转换关系表示成二元决策图的形式。我们给出了在这种数据结构下的可达性分析算法的改进,对该算法进行了时间复杂度分析,并结合一个具体的验证实例对空间复杂度进行了分析,表明改进后的算法的时间复杂度基本不变,同时又降低了可达性分析的空间复杂度。在应用研究部分,首先是介绍了基于时间自动机的验证工具UPPAAL,然后是结合该工具给出了模型验证的步骤和建模的标准,最后构造了飞机着陆控制系统的时间自动机模型,检测了系统是否安全可靠,避免了系统运行时出现错误。通过使用验证工具UPPAAL,我们可以方便地为系统构造模型,有利于设计人员认清系统的运行过程,及时发现系统中存在的一些问题。

全文目录


摘要  3-4
Abstract  4-5
目录  5-7
第一章 前言  7-11
  1.1 研究背景和意义  7-8
  1.2 研究现状  8-9
  1.3 本文结构  9-11
第二章 时间自动机  11-19
  2.1 时间自动机的定义  11-13
    2.1.1 时间转换系统  11
    2.1.2 时间约束和时钟解释  11-12
    2.1.3 时间自动机的语法和语义  12-13
  2.2 时间语言  13-15
  2.3 时间自动机的扩展  15-18
    2.3.1 对角时钟约束  15-16
    2.3.2 叠加时钟约束  16-17
    2.3.3 内部动作  17
    2.3.4 时钟的更新  17-18
  2.4 本章小结  18-19
第三章 基于时间自动机模型的验证方法  19-33
  3.1 模型验证方法  19-21
    3.1.1 模型验证的概念  19-20
    3.1.2 时间自动机建模  20-21
  3.2 符号化语义和验证  21-24
    3.2.1 时钟区域  21-22
    3.2.2 时钟带  22-24
  3.3 可达性分析  24-30
    3.3.1 后向分析法  24-25
    3.3.2 前向分析法  25-27
    3.3.3 差值有界矩阵(DBM)  27-29
    3.3.4 存在的问题  29-30
  3.4 验证工具  30-32
  3.5 本章小结  32-33
第四章 基于BDD的验证技术  33-48
  4.1 二元决策图(BDD)  33-36
    4.1.1 BDD的概念  33-34
    4.1.2 变量顺序对BDD大小的影响  34-36
  4.2 时间自动机的BDD表示方法  36-42
    4.2.1 时间自动机的整数语义  36-38
    4.2.2 状态和转换关系  38-42
  4.3 可达性分析  42-47
    4.3.1 标准算法  42-43
    4.3.2 算法改进及复杂度分析  43-45
    4.3.3 案例分析  45-47
  4.4 本章小结  47-48
第五章 应用研究  48-56
  5.1 验证工具uppaal介绍  48-50
    5.1.1 基本功能  48-49
    5.1.2 最新改进  49-50
  5.2 验证过程  50-52
    5.2.1 模型验证步骤  50-51
    5.2.2 建模标准  51-52
  5.3 飞机着陆控制系统  52-55
    5.3.1 问题描述  52
    5.3.2 模型构造  52-54
    5.3.3 分析验证  54-55
  5.4 本章小结  55-56
第六章 结论和展望  56-57
致谢  57-58
参考文献  58-62
附录 攻读硕士学位期间发表的论文  62

相似论文

  1. 仿真系统模型验证方法和工具研究,TP391.9
  2. 基于ARM的嵌入式实时操作系统的设计与开发,TP316.2
  3. 多核系统中基于温度限制的节能调度算法研究,TP332
  4. 基于光纤通道的文件级数据共享系统的设计与实现,TP333
  5. 基于DSP的嵌入式星载相机控制器的研究,V445.8
  6. 多处理器单调速率任务调度算法研究,TP332
  7. 面向方面的实时系统建模及实现方法研究,TP316.2
  8. 基于时间自动机模型的CBTC系统安全计算机平台的形式化验证,U284.48
  9. 草畜平衡和精准管理模型在肃南县绵羊生产中的应用研究,S826
  10. 实时嵌入式系统VxWorks安全机制的研究与实现,TP316.2
  11. 基于MDE的UML模型到形式化模型的转换方法研究,TP311.52
  12. 闪拍系统的设计与实现,TP311.52
  13. 多处理器全局FP调度算法的研究,TP332
  14. 分布式信息化平台中嵌入式实时中间件研究,TP368.1
  15. 嵌入式实时系统ARTs-OS的动态内存管理研究,TP333.1
  16. 柔性工作流过程模型的研究,TP311.52
  17. IF对实时软件设计图形模型的验证,TP311.52
  18. 基于PI演算的CRM系统的设计与实现,TP311.52
  19. 基于XML的信息转化和编辑系统设计,TP311.52
  20. 实时系统调度算法的抢占控制模型及其遗传算法实现,TP316.2

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 一般性问题 > 理论、方法 > 自动机理论
© 2012 www.xueweilunwen.com