教育论文网

基于图论的形式化验证方法的研究与实现
硕士博士毕业论文站内搜索    
分类：教育论文网→工业技术论文→自动化技术、计算机技术论文→计算技术、计算机技术论文→一般性问题论文→设计与性能分析论文→性能分析、功能分析论文
基于图论的形式化验证方法的研究与实现
论文目录
 
摘要第1-6页
ABSTRACT第6-10页
第一章 绪论第10-15页
　　1.1 研究工作的背景与意义第10页
　　1.2 形式化验证的国内外研究历史与现状第10-13页
　　1.3 本论文的主要工作第13-14页
　　1.4 本论文的结构安排第14-15页
第二章 形式化验证方法的基础第15-26页
　　2.1 形式化方法的基础知识第15-20页
　　　　2.1.1 命题逻辑第15页
　　　　2.1.2 谓词逻辑第15-16页
　　　　2.1.3 时态逻辑第16-20页
　　2.2 CTL验证算法第20-25页
　　　　2.2.1 CTL验证原理的概述第20页
　　　　2.2.2 原子命题节点的验证第20-21页
　　　　2.2.3 CTL布尔逻辑算子的验证算法第21页
　　　　2.2.4 CTL时态逻辑算子EX的验证算法第21-22页
　　　　2.2.5 CTL时态逻辑算子EU的验证算法第22-23页
　　　　2.2.6 CTL时态逻辑算子EG的验证算法第23-24页
　　　　2.2.7 验证算法举例第24-25页
　　2.3 本章小结第25-26页
第三章 基于图的邻接矩阵的形式化方法研究第26-52页
　　3.1 待验证系统建模方法第26-33页
　　　　3.1.1 有向图与邻接矩阵第27-28页
　　　　3.1.2 Kripke结构与有向图第28页
　　　　3.1.3 根据状态集和原子命题建立矩阵第28-30页
　　　　3.1.4 邻接矩阵赋值第30-31页
　　　　3.1.5 无效状态化简第31页
　　　　3.1.6 实例说明第31-33页
　　3.2 待验证规范的描述第33-37页
　　　　3.2.1 规范的单词分类第33-34页
　　　　3.2.2 规范表达式语法分析树第34-35页
　　　　3.2.3 逻辑运算符的优先级第35页
　　　　3.2.4 根据优先级制定语法分析树第35-37页
　　3.3 基于邻接矩阵的验证方法第37-45页
　　　　3.3.1 验证的数据形式第37-38页
　　　　3.3.2 验证流程第38-39页
　　　　3.3.3 原子命题的验证第39-40页
　　　　3.3.4 布尔逻辑操作符的验证第40页
　　　　3.3.5 时态逻辑操作符的验证第40-45页
　　3.4 反例路径求解方法第45-51页
　　　　3.4.1 反例路径求解的原理和主要步骤第45-46页
　　　　3.4.2 待求规范取反第46-48页
　　　　3.4.3 反例路径输出第48-51页
　　3.5 本章小结第51-52页
第四章 基于图的邻接矩阵的形式化验证工具的设计与实现第52-68页
　　4.1 形式化验证工具系统的整体流程图第52-53页
　　4.2 矩阵建模功能模块设计与实现第53-56页
　　　　4.2.1 建模模块的总体设计第53页
　　　　4.2.2 输入文件的设计第53页
　　　　4.2.3 空矩阵的建立第53-54页
　　　　4.2.4 在矩阵中加入转移关系第54-55页
　　　　4.2.5 去除矩阵中的无效状态第55-56页
　　4.3 待求规范转化为语法树第56-59页
　　　　4.3.1 语法树的数据结构第57页
　　　　4.3.2 待求规范的词法分析第57-58页
　　　　4.3.3 待求规范的语法分析第58-59页
　　4.4 验证模块的设计与实现第59-64页
　　　　4.4.1 验证过程的总体设计第59-60页
　　　　4.4.2 四个主要的验证算法实现第60-64页
　　4.5 反例模块的设计与实现第64-67页
　　　　4.5.1 规范取反的设计与实现第64-65页
　　　　4.5.2 取反例路径的几个主要算法的设计第65-67页
　　4.6 本章小结第67-68页
第五章 实例研究第68-86页
　　5.1 FIFO第68-75页
　　　　5.1.1 FIFO的性质第68-69页
　　　　5.1.2 FIFO操作行为的描述第69-71页
　　　　5.1.3 FIFO的规范验证第71-74页
　　　　5.1.4 实例运行结果第74-75页
　　5.2 PCI总线第75-81页
　　　　5.2.1 PCI总线仲裁器简介第75-76页
　　　　5.2.2 PCI总线仲裁器属性和规范描述第76-78页
　　　　5.2.3 PCI总线仲裁器建模第78-79页
　　　　5.2.4 实例运行结果第79-81页
　　5.3 性能测试第81-84页
　　　　5.3.1 数据结果第81-83页
　　　　5.3.2 结果分析第83-84页
　　　　5.3.3 综合分析第84页
　　5.4 特点及适用场合第84页
　　5.5 本章小结第84-86页
第六章 全文总结与展望第86-88页
　　6.1 全文总结第86页
　　6.2 下一步工作及展望第86-88页
致谢第88-89页
参考文献第89-93页
攻读硕士学位期间取得的成果第93-94页

本篇论文共94页，点击这进入下载页面。
 
更多论文
基于图论的形式化验证方法的研究与
数据中心虚拟机的迁移方法研究
云平台下虚拟机调度研究与实现
虚拟化数据中心的集群监控管理系统
基于多VM迁移调度的云数据中心网络
数据中心虚拟机的动态迁移技术研究
基于情境认知理论的移动学习资源设
云计算系统故障注入平台的研究与设
虚拟数据中心的跨域映射算法研究
基于SDN的数据中心流量工程研究
基于SDN数据中心的链路负载均衡研究
基于SDN/OpenFlow的数据中心网络的
基于SDN的多租户数据中心网络研究
基于VMware vSphere的高校数据中心
余数系统中模加和模乘单元设计
片上多核系统高速缓存的功耗管控方
基于STM32微控制器的自由感应加热控
基于ZYNQ-7000全可编程平台的多串口
处理器数据处理单元的微结构优化方
龙芯多核处理器多线程故障恢复系统
面向SPARC V8 ISA的处理器模型验证
基于SystemVerilog语言的同步/异步
基于动态副本机制的web文件系统
空气下稳定的柔性/透明聚合物薄膜电
基于RapidIO的大容量固态存储系统设
分布式环境下的多副本策略研究
基于HDFS的分布式存储系统的研究与
云计算平台中内存缓存系统的设计与
HDFS云存储系统可用性能的优化研究
面向新型非易失性存储器的内存管理
高效的云端数据完整性验证机制研究
云存储中多层次索引可搜索加密的研
基于HDFS的海量小文件处理性能的研
基于USB总线的内存测试模块设计
ZnO基多元金属氧化物阻变开关的制备
铁酸铋薄膜阻变效应与陷阱电荷现象
云环境下基于身份的数据完整性证明
云存储中多维数据查询隐私保护的研
面向高并发小包数据分布式存储系统
透明电阻型存储器件的研究
基于对等结构云存储的副本管理研究
基于墨盒控制芯片的存储器设计及FP
基于Hadoop的气象信息云存储系统设
新型非挥发存储器及系统优化技术研
分布式视频流存储系统的设计与实现
云存储调度关键技术研究与实现
基于FastDFS云存储系统的研究与设计
基于MooseFS的云存储系统的研究与实
高速采样数据存储控制器的设计与实
忆阻器件及其应用
基于MTM反溶丝结构的OTP存储器读出
512Kbit反熔丝OTP存储器设计及实现
OTP存储器智能烧录系统开发技术研究
基于数据依赖关系的云存储优化算法
基于SOPC的NAND Flash控制器设计
分布式溯源信息存储系统的研究与实
氧化物阻变存储器材料中电阻转变与
基于HDFS的海量小文件读写策略研究
混合主存感知的末级缓存管理策略研
基于NVM的写操作优化策略研究与设计
基于网络编码的分布式存储系统中修
含吡啶聚合物的合成及其分子结构调
硬盘动不平衡测量和校正方法研究
分布式存储系统中的失效节点修复研
基于PXIe总线的高速固态存储卡研制
基于Swift的小对象访问性能优化研究
基于HDFS的分布式存储中负载均衡技
生物分子与共轭聚合物双层结构有机
TFC磁头磁盘界面气体薄膜多物理场耦
YFe0.5Cr0.5
近阈值8管存储器设计
基于ECC电路的软错误修复和测试诊断
基于页组映射的固态盘闪存转换层优
NAND Flash错误特性模型及应用研究
基于Swift的海量小文件对象存储研究
DPDK结构下类Socket接口研究与设计
面向InfiniBand控制器的PCI Expres
基于固件文件系统的UEFI安全机制研
基于FPGA结构高速PCIe总线传输系统
USB存储设备安全机制的研究与实现
PCI Express总线分析仪硬件设计
PXIExpress总线接口DMA控制器及驱动
基于振动测试系统的3D打印机优化技
基于数值模拟的塑料颗粒3D打印机关
基于LED光的三维扫描仪控制系统研究
桌面级三维激光扫描仪样机及扫描算
量子存储板高速数据传输接口关键技
PCI Express总线分析仪软件设计
一体化信息处理平台总线架构设计与
 
形式化验证论文 模型检测论文 Kripke结构论文 CTL表达式论文 邻接矩阵论文
版权申明：目录由用户风云**提供，www.51papers.com仅收录目录，作者需要删除这篇论文目录请点击这里。
| 设为首页||加入收藏||站内搜索引擎||站点地图||在线购卡|
版权所有 教育论文网 Copyright(C) All Rights Reserved