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

基于有限精度时间自动机模型验证技术的研究与应用

专 业: 计算机应用
关键词: 形式化描述 模型验证 实时系统 时间自动机
分类号: TP301
形 态: 共 49 页 约 32,095 个字 约 1.535 M内容
阅 读: 全文阅读说明

内容摘要


一种对实时系统进行形式化验证具有很大潜力的方法是使用时间自动机网络对系统进行建模,然后通过遍历系统的状态空间来检查是否某些状态不满足系统的需求。

虽然时间自动机模型的自动验证算法已经被提出了,但是这些算法还面临着两种潜在的由并行合成引起的爆炸问题:

控制节点空间的爆炸和时钟变量上时间域空间的爆炸。

在该文中,一种时间自动机模型的变体被用来解决时钟变量上时间域空间爆炸的问题。

这种模型被称为有限精度时间自动机,它是用整型值时钟扩展的有限状态自动机。

我们提出了这种模型自动验证的完整方法,并开发出一套自动验证工具。

虽然由于时间值的近似性,这种模型在表达能力上比连续时间的模型稍微弱一些,但是,对于一些例子,它的模型验证算法的实现在时间和空间上都表现得很好。

这是因为这种模型减小了一个系统状态的物理表示大小,并且避免了费时的时间域之间的包含检查。

最后,为了在足够复杂的形式化描述和验证的环境下对我们的自动验证工具进行检验,我们分析了多媒体和通信领域的两个应用实例……

全文目录


文摘
英文文摘
前言
第一章 相关知识介绍
1.1.形式化方法
1.2.时间自动机
1.2.1.状态转移系统定义
1.2.2.时钟约束及时钟映射的定义
1.2.3.语义与语法
第二章 有限精度时间自动机模型
2.1.有限精度时间自动机
2.2.相关定义和几点说明
2.3.有限精度时间自动机网络
第三章 有限精度时间自动机模型验证的算法
3.1.有限精度时间自动机网络的语义
3.2.状态空间遍历算法
3.3.时钟顺序的标准化
3.4.模型验证
3.4.1.性质描述逻辑
3.4.2.模型验证算法
第四章 有限精度时间自动机模型验证算法的实现技术
4.1.自动机网络的表示
4.2.系统状态的表示
4.3.系统状态空间的表示
4.4.系统性质的表示
4.5.模型验证算法的改进
4.5.1.WAIT结构的改进
4.5.2.使用缓冲区减少编解码次数
4.5.3.宽度优先与深度优先相结合减少编解码次数
第五章 有限精度时间自动机模型验证工具
5.1.功能模块
5.2.系统描述语法
5.3.主要的数据结构
第六章 实例分析
6.1.唇同步协议分析
6.1.1.唇同步协议
6.1.2.形式化描述
6.1.3.模型验证
6.1.4.模型验证结果
6.2.载波监听多点接入/冲突避免(CSMA/CA)协议分析
6.2.1.CSMA/CA协议
6.2.2.形式化描述
6.2.3.模型验证
第七章 总结
参考文献
附录
附录1唇同步协议在工具中的描述文本
附录2 CSMA/CA协议在工具中的描述文本

相似论文

  1. Web结构挖掘中HITS算法的研究,68页,TP301.6 TP393.03
  2. 潜在语义分析中算法的并行化研究与实现,59页,TP301.2 TP301.6
  3. 智能算法在入侵检测系统中的应用,70页,TP301.6
  4. 基于遗传算法智能组卷的研究与应用,50页,TP301.6 TP18
  5. 带随机步的可满足性算法,46页,TP301.6
  6. 并联机构的运动学精度提高方法研究,68页,TP301.6 TP242.2
  7. 生物分子网络的相似子网搜索算法研究及应用,52页,TP301.6 TP399 R318
  8. 集成电路层次式热驱动布图布局算法研究,54页,TP301.6
  9. 基于改进微粒群算法的配送中心选址研究,52页,TP301.6 F252.24
  10. 基于网格计算平台的智能优化算法应用与研究,66页,TP301.6
  11. 鲁棒性水印算法研究与实现,65页,TP301.6
  12. 应用主导的CA互通技术研究,60页,TP309.2
  13. 进化算法中多种信息的利用,60页,TP301.6
  14. 具有学习机制的分布式入侵检测系统研究,52页,TP309
  15. 非结构网络生成技术及在浅水波方程求解中的应用,82页,TP301.6 TP393.02
  16. 手机病毒的分析及对策研究,72页,TP309.5
  17. X.509证书和RBAC在Web中的应用,57页,TP309 TP393.08
  18. BSP并行库及其回卷恢复机制在SMP集群系统上的实现,55页,TP302.1
  19. 网格门户的研究和设计—流体流向模拟门户,49页,TP302.1
  20. 低功耗微处理器体系结构的研究与设计,115页,TP301 TP332
中图分类: > TP301 > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 一般性问题 > 理论、方法

© 2012 book.hzu.edu.cn