形式化方法导论
￥ 48.01 7.0折 ￥ 69 九五品
仅1件
作者张广泉
出版社清华大学出版社
ISBN9787302626602
出版时间2023-03
版次1
装帧平装
开本16开
纸张胶版纸
页数300页
字数99999千字
定价69元
上书时间2024-05-07
商品详情
- 品相描述：九五品
- 商品描述
-
基本信息
书名:形式化方法导论
定价：69.00元
作者:张广泉
出版社：清华大学出版社
出版日期：2023-03-01
ISBN：9787302626602
字数：458000
页码：300
版次：2
装帧：平装
开本：16开
商品重量：
编辑推荐
内容提要
形式化方法是指有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动。随着软件可信需求的不断增长，形式化方法的重要性和关注度日益提高。本书共12章，章概述形式化方法，第2章介绍形式化方法发展早期的经典内容，其余部分共分3篇： 上篇（第3～5章）为系统建模篇，着重介绍迁移系统、有穷自动机、Petri网等基本计算模型； 中篇（第6和第7章）为形式规约篇，着重讨论时序逻辑及其在并发系统属性描述的应用； 下篇（第8～12章）为形式验证篇，着重介绍定理证明方法和并发、实时及混成系统的各种模型检测方法及相关验证工具。全书提供了大量应用实例，每章后均附有习题。本书适合作为高等院校计算机、软件工程、人工智能、网络工程、信息安全、自动化等专业高年级本科生、研究生的教材，同时可供相关领域的研究人员和技术开发人员参考。
目录
目录章绪论1.1形式化方法的发展历程1.2形式化方法的基本内容1.2.1系统建模1.2.2形式规约1.2.3形式验证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验证工具SPIN9.3.2应用举例9.4本章小结习题90章符号模型检测10.1二叉判定图10.1.1基本概念10.1.2约简方法10.1.3Apply操作及应用10.2CTL符号模型检测10.2.1基本方法10.2.2验证工具SMV10.2.3应用举例10.3LTL符号模型检测简介10.4本章小结习题101章概率模型检测11.1概率模型11.1.1离散时间马尔可夫链11.1.2马尔可夫决策过程11.1.3连续时间马尔可夫链11.2概率时序逻辑11.2.1概率计算树逻辑11.2.2连续随机逻辑11.3概率模型检测工具及应用11.3.1验证工具PRISM11.3.2应用举例11.4本章小结习题112章实时与混成系统验证12.1时间自动机12.1.1语法12.1.2语义12.2实时逻辑12.2.1时间计算树逻辑12.2.2度量区间时序逻辑12.3实时系统模型检测12.3.1基本方法12.3.2验证工具UPPAAL12.3.3应用举例12.4混成系统验证简介12.4.1混成自动机12.4.2微分动态逻辑12.4.3混成系统模型检测12.5本章小结习题12参考文献
作者介绍
序言
-
【封面】
相关推荐
— 没有更多了 —
以下为对购买帮助不大的评价