新书推荐 |
您所在的位置:网站首页 › crc校验码手动计算例题 › 新书推荐 |
1.3本章小结 习题1 第2章程序正确性证明 2.1Floyd前后断言法 2.1.1基本概念 2.1.2证明方法 2.1.3应用举例 2.2Hoare公理化方法 2.2.1基本概念 2.2.2证明方法 2.2.3应用举例 2.3Dijkstra最弱前置条件方法 2.3.1基本概念 2.3.2证明方法 2.3.3应用举例 2.4本章小结 习题2 上篇系 统 建 模 第3章迁移系统 3.1基本概念 3.1.1形式定义 3.1.2迁移图 3.1.3计算 3.2应用举例 3.2.1时序电路 3.2.2数据依赖系统 3.2.3并发和交错 3.3本章小结 习题3 第4章自动机 4.1有穷自动机 4.1.1有穷状态系统 4.1.2形式定义 4.1.3判定算法 4.2Büchi自动机 4.2.1ω有穷自动机简介 4.2.2Büchi自动机 4.2.3应用举例 4.3本章小结 习题4 第5章Petri网 5.1库所/变迁Petri网 5.1.1基本概念 5.1.2基本性质 5.1.3分析方法 5.1.4应用举例 5.2谓词/变迁Petri网 5.2.1基本概念 5.2.2应用举例 5.3着色Petri网 5.3.1基本概念 5.3.2应用举例 5.4本章小结 习题5 中篇形 式 规 约 第6章时序逻辑 6.1线性时序逻辑 6.1.1LTL语法 6.1.2LTL语义 6.1.3应用举例 6.2分支时序逻辑 6.2.1CTL语法 6.2.2CTL语义 6.2.3应用举例 6.3区间时序逻辑简介 6.4本章小结 习题6 第7章并发系统属性 7.1基本概念 7.2安全性 7.2.1形式定义 7.2.2形式描述 7.2.3应用举例 7.3活性 7.3.1形式定义 7.3.2形式描述 7.3.3应用举例 7.4本章小结 习题7 下篇形 式 验 证 第8章定理证明 8.1时序逻辑演绎验证方法 8.1.1PLTL逻辑系统 8.1.2MannaPnueli演绎规则方法 8.1.3验证工具STeP及应用 8.2自动定理证明方法 8.2.1SAT求解算法 8.2.2SMT求解技术 8.2.3ATP方法小结 8.3交互式定理证明方法 8.3.1主要证明辅助工具简介 8.3.2应用举例 8.3.3ITP方法小结 8.4本章小结 习题8 第9章模型检测 9.1基本概念 9.2模型检测算法 9.2.1CTL模型检测算法 9.2.2LTL模型检测算法 9.3模型检测工具及应用 9.3.1验证工具SPIN 9.3.2应用举例 9.4本章小结 习题9 第10章符号模型检测 10.1二叉判定图 10.1.1基本概念 10.1.2约简方法 10.1.3Apply操作及应用 10.2CTL符号模型检测 10.2.1基本方法 10.2.2验证工具SMV 10.2.3应用举例 10.3LTL符号模型检测简介 10.4本章小结 习题10 第11章概率模型检测 11.1概率模型 11.1.1离散时间马尔可夫链 11.1.2马尔可夫决策过程 11.1.3连续时间马尔可夫链 11.2概率时序逻辑 11.2.1概率计算树逻辑 11.2.2连续随机逻辑 11.3概率模型检测工具及应用 11.3.1验证工具PRISM 11.3.2应用举例 11.4本章小结 习题11 第12章实时与混成系统验证 12.1时间自动机 12.1.1语法 12.1.2语义 12.2实时逻辑 12.2.1时间计算树逻辑 12.2.2度量区间时序逻辑 12.3实时系统模型检测 12.3.1基本方法 12.3.2验证工具UPPAAL 12.3.3应用举例 12.4混成系统验证简介 12.4.1混成自动机 12.4.2微分动态逻辑 12.4.3混成系统模型检测 12.5本章小结 习题12 参考文献 扫码优惠购书返回搜狐,查看更多 |
CopyRight 2018-2019 办公设备维修网 版权所有 豫ICP备15022753号-3 |