第一个书签之前
第一章 绪论
§1.1研究背景及意义
§1.2国内外研究现状
§1.2.1运行时验证的定义
§1.2.2运行时验证的分类
§1.2.3运行时验证的研究
§1.3研究内容与主要贡献
§1.4论文结构
第二章 研究理论基础
§2.1性质描述语言
§2.1.1线性时态逻辑
§2.1.2上下文无关文法
§2.1.3扩展的正则表达式
§2.2语言及自动机
§2.2.1 Kripke结构及语言
§2.2.2自动机理论
§2.3运行时验证工具JavaMOP
§2.4本章小结
第三章 基于自动机的运行时验证监控器生成方法
§3.1 LTL公式生成运行时验证监控器
§3.1.1性质描述语言生成监控器
§3.1.2交错公式Alternating formula
§3.2 LTL公式到VWAA的转换
§3.3 VWAA到TGBA的转换
§3.4 TGBA到Büchi自动机的转换
§3.5 Büchi自动机到DFA的转换
§3.5.1 Büchi自动机到NFA
§3.5.2 NFA转换为DFA
§3.6本章小结
第四章 高效运行时验证工具构造方法
§4.1 LTL公式重写
§4.2 LTL到Büchi自动机的优化
§4.3自动机化简策略
§4.4实验结果
§4.4.1形式化规约
§4.4.2时间与内存消耗
§4.5本章小结
第五章 运行时验证工具RVC
§5.1 RVC的整体架构
§5.2 SafeEnum运行时验证
§5.2.1 SafeEnum监控器构造
§5.2.2 SafeEnum运行时验证过程
§5.3本章小结
第六章 案例分析
§6.1阵列重构技术
§6.1.1基础知识
§6.1.2处理器阵列架构与重构机制
§6.2基于SAT的PETA求解方法
§6.2.1目标阵列的SAT模型及编码
§6.2.2求解出的PETA
§6.3高效能处理器阵列结果的验证
§6.4正确性验证结果
§6.5本章小结
第七章 总结与展望
§7.1总结
§7.2展望
参考文献
致 谢
作者在攻读硕士期间主要研究成果
