新書推薦：
《
安全感是内心长出的盔甲
》
售價：NT$
305.0
《
快人一步：系统性能提高之道
》
售價：NT$
505.0
《
我们为什么会做梦：让梦不再神秘的新科学
》
售價：NT$
352.0
《
算法图解（第2版）
》
售價：NT$
356.0
《
科学的奇幻之旅
》
售價：NT$
352.0
《
画艺循谱：晚明的画谱与消闲
》
售價：NT$
653.0
《
新民说·现实政治史：从马基雅维利到基辛格
》
售價：NT$
454.0
《
宽容是件奢侈品（人生360度·一分钟经典故事）
》
售價：NT$
203.0
|
| 編輯推薦： |
|
形式化方法是软件工程专业的核心课程，但相关教材稀缺，本书弥补了这一空白，内容全面，适合教学。
|
| 內容簡介： |
|
形式化方法是指有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动。随着软件可信需求的不断增长，形式化方法的重要性和关注度日益提高。 本书共12章，第1章概述形式化方法，第2章介绍形式化方法发展早期的经典内容，其余部分共分3篇： 上篇（第3～5章）为系统建模篇，着重介绍迁移系统、有穷自动机、Petri网等基本计算模型； 中篇（第6和第7章）为形式规约篇，着重讨论时序逻辑及其在并发系统属性描述的应用； 下篇（第8～12章）为形式验证篇，着重介绍定理证明方法和并发、实时及混成系统的各种模型检测方法及相关验证工具。全书提供了大量应用实例，每章后均附有习题。 本书适合作为高等院校计算机、软件工程、人工智能、网络工程、信息安全、自动化等专业高年级本科生、研究生的教材，同时可供相关领域的研究人员和技术开发人员参考。
|
| 目錄：
|
第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.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
参考文献
|
| 內容試閱：
|
近年来，形式化方法的一个重要内容——基于定理证明的形式验证方法取得了较大进展和突破。一方面，随着自动证明理论的发展和计算机处理器能力的大幅增强，基于自动定理证明器的自动验证能力大幅提升，如微软公司开发的SMT求解器Z3已成为目前使用最广泛的自动定理证明器； 另一方面，基于人机交互的半自动证明在可验证的系统软件上取得显著突破，如分别在交互式定理证明器Coq和Isabelle/HOL的支持下，INRIA对C语言编译器CompCert的验证及NICTA对操作系统微内核seL4的验证等。
本次修订除更正第1版的一些文字及印刷错误和叙述不当之处外，主要修订第8章及与之关联的部分章节内容，重点阐述了一些典型的定理证明方法、工具和应用。此外，还补充介绍了我国科学家在形式化方法领域的部分开创性研究工作。
本书修订工作得到江苏省高等学校重点教材立项建设、江苏高校优势学科建设工程项目资助和江苏省计算机学会立项资助，以及苏州大学教务处和计算机科学与技术学院的关心和支持，中国科学院软件研究所晏荣杰副研究员对本书修订提出了宝贵的建议，清华大学出版社安妮编辑为本书再版做了大量工作，在此一并表示诚挚的感谢。
张广泉
2023年1月于苏州大学天赐庄校区
第1版前言
软件产业是信息产业的核心，是国家信息化的基础和支撑。软件是工业4.0和中国制造2025的使能和驱动。为推进产业结构优化升级，加快培养软件人才的步伐，近年来大力发展高校软件工程教育，软件工程已从最初的计算机科学与技术的一个学科方向调整为包括软件工程理论与方法、软件工程技术、软件服务工程和领域软件工程等学科方向的、独立的一级学科。软件工程理论与方法是软件工程一级学科的基础，作为其核心内容之一，形式化方法是指有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动。随着软件可信需求的不断增长，形式化方法的重要性和关注度日益提高。
形式化方法相关的教学工作已经得到欧美国家高等学校的重视和推广，知识体系和课程教学内容日趋完善。而目前国内高校关于形式化方法教育还相对薄弱，主要因素之一是缺乏比较全面、系统介绍形式化理论、方法和应用的教材。
本书是在学习、总结形式化方法领域国内外相关文献的基础上，结合作者多年从事形式化方法教学和科研的实践撰写而成的，本书具有以下几个特点：
（1） 通过详细分析和梳理，提炼出形式化方法核心、本质的原理、方法和技术，其中自动机和时序逻辑是贯穿全书内容的两大重要基础。
（2） 重点阐述以模型检测为主要内容的形式化验证方法，使学生在有限的学时范围内，能有效地掌握形式化方法自动化部分的核心内容。
（3） 注重实践与应用，详细介绍SPIN、UPPAAL和PRISM等典型的形式化验证工具的使用方法，结合实例分析，达到理论学习与实际应用的有机结合。
全书共12章。其中第1章概述形式化方法的发展历程和基本内容，第2章介绍形式化方法发展早期的经典内容，即串行程序的正确性证明。其余部分针对并发系统，分为上、中、下三篇阐述形式化建模、规约和验证方法。其中：
上篇（第3～5章）为系统建模篇，主要介绍三个典型的并发系统计算模型。第3章介绍基于状态迁移的计算模型——迁移系统，第4章介绍描述有穷状态系统的计算模型——有穷自动机，它也是计算机科学中最基本的数学模型，第5章介绍最早的并发计算模型——Petri网。
中篇（第6和第7章）为形式规约篇，着重讨论并发系统属性的主要规约方法及应用。第6章介绍真假值依赖时间而变化的非经典逻辑——时序逻辑，它是描述并发系统属性的重要工具，第7章重点阐述并发系统最基本的两类属性——安全性和活性，及其时序逻辑描述方法。
下篇（第8～12章）为形式验证篇，着重介绍主要的形式验证方法及相关验证工具。第8章介绍基于时序逻辑的演绎证明方法及验证工具STeP，第9~12章重点阐述模型检测方法、工具及其在并发、实时及混成系统中的应用，这是形式化方法自动化的核心内容，也是本书的重点。其中第9章介绍经典的模型检测算法、验证工具SPIN及应用，第10章介绍基于二叉判定图(BDD)的符号模型检测方法、验证工具SMV及应用，第11章介绍模型检测与概率分析方法相结合的概率模型检测方法、验证工具PRISM及应用，第12章介绍实时与混成系统的模型检测方法、验证工具UPPAAL及应用。
全书提供了大量应用实例，每章后均附有习题。
本书由张广泉担任主编，负责全书内容的组稿、统稿和修改工作。顾玉磊、宋相君、宋振华、项周坤、沈兴勤、郑林峰、张红美等参与了书稿整理、文字录入和校对工作，祝义副教授、孙庆英老师、魏慧老师等参与了部分书稿的校对工作，在此对他们的辛勤劳动表示感谢。此外，在本书的编写过程中，参考了大量国内外相关文献，在此对本书所引用文献的作者深表感谢。
本书编写工作得到江苏省“十二五”高等学校重点教材立项建设和苏州大学教材培育项目的资助，以及江苏省自然科学基金（BK2011281）、中国科学院软件研究所计算机科学国家重点实验室开放课题（SYSKF0908、SYSKF1201）、南京大学计算机软件新技术国家重点实验室开放课题（KFKT2012B15）的支持和帮助。中国科学院软件研究所焦莉研究员、李广元副研究员、朱雪阳博士、晏荣杰博士仔细阅读了本书初稿，提出了许多重要的修改意见与建议，在此表示衷心感谢。本书的编写还得到中国科学院软件研究所周巢尘院士、林惠民院士、沈一栋研究员、张健研究员、张文辉研究员、詹乃军研究员、南京大学李宣东教授、上海大学缪淮扣教授、南京航空航天大学黄志球教授、东南大学李必信教授等及苏州大学教务部和计算机科学与技术学院的关心和支持，清华大学出版社黄芝和薛阳编辑为本书出版做了大量工作，在此一并表示诚挚的感谢。
由于编者水平有限，书中难免有不当之处，敬请读者批评指正。
张广泉
2015年10月于苏州大学天赐庄校区
|
|
購物車/收銀台(0) | 在線留言板
| 付款方式
| 聯絡我們
| 運費計算
| 幫助中心 |
加入書簽
HOME
新書上架
