中图网

>

计算机教材

形式化方法导论(第2版)

作者：张广泉

出版社：清华大学出版社出版时间：2023-03-01

开本：其他页数： 300

本类榜单：计算机/网络销量榜

中图价:¥53.8(7.8折) 定价 ~~¥69.0~~ 登录后可看到会员价

加入购物车收藏

运费6元，满69元免运费

?快递不能达地区使用邮政小包，运费14元起

云南、广西、海南、新疆、青海、西藏六省，部分地区快递不可达

本类五星书更多>

>
全国计算机等级考试最新真考题库模拟考场及详解·二级MSOffice高级应用

全国计算机等级考试最新真考题库模拟考场及详解·二级MSOffice高级应用

¥11.3¥45
>
决战行测5000题(言语理解与表达)

决战行测5000题(言语理解与表达)

¥28.2¥88
>
软件性能测试.分析与调优实践之路

软件性能测试.分析与调优实践之路

¥55.2¥69
>
第一行代码Android

第一行代码Android

¥76.2¥99
>
C Primer Plus 第6版中文版

C Primer Plus 第6版中文版

¥75.6¥108
>
深度学习

深度学习

¥82.3¥168
>
MATLAB计算机视觉与深度学习实战-赠在线交流卡和本书源码

MATLAB计算机视觉与深度学习实战-赠在线交流卡和本书源码

¥43.5¥79

商品详情
商品评论(0条)

中图价:¥53.8 加入购物车

版权信息
本书特色
内容简介
目录

微信公众号

形式化方法导论(第2版) 版权信息

ISBN：9787302626602
条形码：9787302626602 ; 978-7-302-62660-2
装帧：一般胶版纸
册数：暂无
重量：暂无
所属分类：
计算机/网络
>
计算机教材

形式化方法导论(第2版) 本书特色

形式化方法是软件工程专业的核心课程，但相关教材稀缺，本书弥补了这一空白，内容全面，适合教学。全面讲解形式化方法，评为江苏省高等学校重点教材

形式化方法导论(第2版) 内容简介

形式化方法是指有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动。随着软件可信需求的不断增长，形式化方法的重要性和关注度日益提高。本书共12章，第1章概述形式化方法，第2章介绍形式化方法发展早期的经典内容，其余部分共分3篇：上篇（第3～5章）为系统建模篇，着重介绍迁移系统、有穷自动机、Petri网等基本计算模型；中篇（第6和第7章）为形式规约篇，着重讨论时序逻辑及其在并发系统属性描述的应用；下篇（第8～12章）为形式验证篇，着重介绍定理证明方法和并发、实时及混成系统的各种模型检测方法及相关验证工具。全书提供了大量应用实例，每章后均附有习题。本书适合作为高等院校计算机、软件工程、人工智能、网络工程、信息安全、自动化等专业高年级本科生、研究生的教材，同时可供相关领域的研究人员和技术开发人员参考。

形式化方法导论(第2版) 目录

第1章绪论

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.2MannaPnueli演绎规则方法

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

参考文献

展开全部

商品评论(0条)

写书评赚书币

暂无评论……

书友推荐

>
龙榆生：词曲概论/大家小书
龙榆生：词曲概论/大家小书
龙榆生
¥9.1~~¥24.0~~
>
经典常谈
经典常谈
朱自清
¥17.1~~¥39.8~~
>
罗庸西南联大授课录
罗庸西南联大授课录
罗庸
¥13.8~~¥32.0~~
>
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
企鹅口袋书系列·伟大的思想20:论自然选择(英汉双语)
[英] 达尔文著，朱邦芊译
¥8.4~~¥14.0~~
>
莉莉和章鱼
莉莉和章鱼
[美]史蒂文·罗利
¥16.0~~¥42.0~~
>
【精装绘本】画给孩子的中国神话
【精装绘本】画给孩子的中国神话
施英巍
¥20.9~~¥55.0~~
>
名家带你读鲁迅:朝花夕拾
名家带你读鲁迅:朝花夕拾
鲁迅著，陈漱渝主编
¥14.3~~¥21.0~~
>
唐代进士录
唐代进士录
陶易
¥26.7~~¥39.8~~