教育论文网

基于SAT的符号化模型检验技术研究

硕士博士毕业论文站内搜索    
分类:教育论文网→工业技术论文→自动化技术、计算机技术论文计算技术、计算机技术论文一般性问题论文理论、方法论文
基于SAT的符号化模型检验技术研究
论文目录
 
摘要第1-11页
ABSTRACT第11-14页
第一章 绪论第14-34页
  · 研究背景第14-16页
  · 模型检验技术第16-24页
    · 模型描述第16-17页
    · 规约描述第17-18页
    · 模型检验算法第18-20页
    · 典型工具第20-24页
  · 研究动机与研究内容第24-28页
    · 优化的LTL限界模型检验技术第25页
    · ω-正规性质的限界模型检验技术第25-26页
    · 限界模型检验的完全性保证技术第26-27页
    · 工具实现第27-28页
  · 相关工作第28-30页
    · 限界模型检验技术第28页
    · ω-正规性质的符号化模型检验技术第28-29页
    · 限界模型检验的完全性保证技术第29-30页
  · 论文贡献第30-32页
  · 论文结构第32-34页
第二章 基础知识第34-62页
  · 基本概念第34-44页
    · 字、布尔公式第34-35页
    · 非确定的 ω-自动机第35-36页
    · 时序逻辑第36-41页
    · 迁移系统第41-43页
    · 线性时序逻辑的模型检验问题第43-44页
  · 基本算法第44-61页
    · DPLL算法第44-48页
    · 基本的BMC编码第48-52页
    · 基于反例的抽象精化算法第52-53页
    · 基于证明的抽象精化算法第53页
    · 基于归纳的模型检验算法第53-54页
    · 基于插值的模型检验算法第54-56页
    · 属性制导的可达性分析算法第56-61页
  · 本章总结第61-62页
第三章 优化的LTL限界模型检验技术第62-86页
  · 研究动机第62-63页
  · 反例保持的LTL化简技术第63-73页
    · 基本规则第63-66页
    · 派生原则第66-69页
    · 化简策略第69-70页
    · 性能分析第70-73页
  · 增量式的基于语义的编码技术第73-76页
    · 基本的基于语义的编码第73-74页
    · 增量式的基于语义的编码第74-76页
  · 实验结果第76-84页
    · C?PR?实验结果第77-83页
    · 增量式的基于语义的BMC实验结果第83-84页
  · 本章总结第84-86页
第四章 ω-正规性质的限界模型检验技术第86-106页
  · 研究动机第86-87页
  · ETLl+f限界模型检验第87-96页
    · ETLl+f的tableau构造第87-95页
    · 基于语义的ETLl+f的BMC编码第95-96页
  · QTL限界模型检验第96-102页
    · 基于语法的QTL限界模型检验第96-98页
    · 基于语义的QTL的限界模型检验第98-102页
  · 实验结果第102-105页
  · 本章总结第105-106页
第五章 基于SAT的完全性保证技术第106-132页
  · 研究动机第106-111页
  · 交叠的双向PDR算法第111-118页
  · 并行的双向PDR算法第118-125页
    · 前向PDR算法 (FPDR)第119-121页
    · 后向PDR算法 (BPDR)第121-124页
    · 算法正确性第124-125页
  · 优化方法第125-126页
    · 结合BMC技术的优化策略第125-126页
    · 确定两个任务链表Qf和Qb中任务优先级的策略第126页
    · 启发式的归纳子句生成算法第126页
  · 实验结果第126-130页
  · 本章总结第130-132页
第六章 工具实现第132-146页
  · 工具实现第132-143页
    · ENu SMV1.2第132-138页
    · Reach第138-143页
  · 工具使用第143-145页
  · 本章总结第145-146页
第七章 总结与展望第146-150页
  · 本文总结第146-148页
  · 将来的工作第148-150页
致谢第150-154页
参考文献第154-166页
作者在学期间取得的学术成果第166-168页
附录A 附录第168-171页
  A.1 DME电路问题第168-170页
  A.2 二进制累加器问题第170-171页

本篇论文共171页,点击这进入下载页面
 
更多论文
基于SAT的符号化模型检验技术研究
信息物理融合系统资源调度关键技术
非线性流形结构在高光谱图像异常检
面向多域联合的服务可信关键技术研
基于随机游动的社会网络个性化排名
大规模数据处理系统中MapReduce任务
开放式海量数据处理服务的计算完整
多组图贝叶斯分类模型研究
在线半监督学习理论、算法与应用研
分布式在线社交网络数据存储及优化
面向车载应用的自适应高动态范围视
关键基础设施网络安全模型与安全机
基于增强学习和车辆动力学的高速公
面向任务的快速响应空间卫星部署优
无线物理层安全传输关键技术研究
面向无线网状网的拒绝服务异常检测
基于加速试验的可靠性验证理论与方
复杂网络链路分析与社交媒体预测
基于结构矩阵的快速算法及其应用
FPGA加速蒙特卡罗计算关键技术的研
间断伽略金方法在瞬态电磁问题中的
光纤水听器阵列超远程光传输低噪声
微纳光纤倏逝场特性及微污染传感技
非饱和黏土动态力学特性及其本构关
耐高温有机硅胶粘剂的制备及性能研
PIP工艺制备SiC/SiC复合材料的结构
基于聚苯胺的兼容型红外电致变色器
精密柔索传动机理与设计方法研究
地磁测量中载体干扰磁场特性及补偿
飞行器关键子系统健康管理中的故障
航天器对星座多星接近轨道设计问题
粉末燃料冲压发动机内镁颗粒群着火
航天器近距离操作自主防撞控制方法
航天器相对运动姿轨一体化动力学建
低空无人机载UWB SAR增强成像技术研
航天器挠性附件结构参数优化设计及
多任务深空探测轨道设计优化方法研
高超声速飞行器机翼非线性颤振研究
基于Fourier-Bessel级数的声波传播
地月平动点动力学与交会控制研究
直升机传动系统状态增强检测的随机
高超声速巡航飞行器姿态控制方法研
超声速流动分离及其控制的试验研究
空间交会任务解析摄动分析与混合整
航天器推进系统基于定性模型的故障
超声速气流中的点火启动及其强化机
基于机载视觉的无人机自主着舰引导
面向装备健康状态评估的可测性设计
AUV舷侧阵浅海远程目标定位方法研究
基于DSM的效能仿真多范式组合建模方
宽带数字侦察接收机及信号分析处理
支持强偏序约束的智能规划与调度方
惯性/多普勒组合导航回溯算法研究
基于新型可饱和脉冲变压器和螺旋Bl
基于能力的武器装备组合规划问题与
装备科研投资激励研究
基于超网络的军事通信网络建模、分
高功率微波输出窗真空表面闪络研究
小天体附近周期轨道及其熵研究
系统级电磁兼容现场测量关键技术研
现代卫星导航信号恒包络发射与抗多
弹载宽带雷达信号处理机关键技术研
复杂传输线网络耦合建模与分析方法
延迟容忍网络信息传输性能分析与优
面向入侵目标追捕的多回路无线网络
直扩信号扩频序列盲估计研究
多功能雷达电子情报信号处理关键技
面向灾难营救场景的延迟容忍网络路
基于压缩感知的高分辨雷达成像方法
卫星导航系统星间组网关键技术研究
多角度SAR成像及特征提取
星载多模式合成孔径雷达成像技术研
多用户MIMO系统下行链路物理层安全
超宽带合成孔径雷达浅埋目标特征获
多发多收合成孔径雷达成像及动目标
面向千万亿次CPU-GPU异构系统的编程
面向瞬时故障的可配置容错技术研究
面向延迟优化的多核处理器Cache数据
面向异构体系结构的稀疏矩阵算法研
嵌入式实时系统通信机制与优化技术
符号执行可扩展性及可行性关键技术
基于几何代数的计算机视觉问题研究
基于多视图几何的视觉辅助惯导组合
基于轮廓和边缘的空间非合作目标视
社交媒体中的信息检索与传播分析
大规模空间数据的高性能查询处理关
软件行为动态分析关键技术研究
基于异构关系的微博网络意见动力学
数据流上序敏感查询处理关键技术研
基于位置的移动信息服务技术与应用
 
模型检验论文 SAT求解器论文 LTL论文 QTL论文 PDR论文
版权申明:目录由用户jdw5**提供,www.51papers.com仅收录目录,作者需要删除这篇论文目录请点击这里
| 设为首页||加入收藏||站内搜索引擎||站点地图||在线购卡|
版权所有 教育论文网 Copyright(C) All Rights Reserved