软件可靠性方法

出版者:机械工业出版社

作者:（以色列）Doron A. Peled

页数:196

译者:王林章 等

出版时间:2012-3

价格:45.00元

装帧:平装

isbn号码:9787111365532

丛书系列:计算机科学丛书

具体描述

【名人推荐】

我第一次翻开这本书时，立刻被这本书的覆盖范围之广所深深打动，它覆盖了规约和建模、演绎验证、模型检验、进程代数、程序测试、状态与消息序列图。除了对每个方法进行了相当深入的介绍以外，本书还讨论了应当在何时选取何种方法以及在选择这些方法时所必须做出的权衡。书中结合当前工具，使用很多具有挑战性的实例来说明各种技术。我还没看见过其他任何覆盖同样内容的书籍能达到如此的深度。

同时，本书描述了应用形式化方法的过程：从建模和规约开始，然后选择一个合适的验证技术，最后测试程序。这些知识在实践中是十分必要的，但是却很少在软件工程的课本里面出现。我确信这本书将会取得巨大的成功。我向所有对软件可靠性问题感兴趣的读者强烈推荐这本书。

—— Edmund M. Clarke教授

图灵奖获得者，卡内基-梅隆大学

【内容简介】

用于创建可靠软件的形式化方法一直处于不断的开发和改进之中。最近，人们对于形式化方法工具的重要组成有了更深入的理解，从软硬件开发业界逐渐接受可靠性工具这一点就可以体现出来。

本书介绍了各种能解决软件可靠性问题的方法。理想情况下，形式化方法应该用起来直观，学起来简洁、快速，对开发过程的影响微乎其微。本书对各种方法进行了比较，揭示了它们各自的优点和缺点，同时紧扣自动机理论和逻辑这两个主题。在尽可能减少背景知识介绍的前提下，本书向非专家读者描述了多种技术，并且针对软件工程领域的研究人员和专业人士介绍了一些高级技术。

本书主题和特点：

 集中介绍目前常用的重要软件可靠性方法，并将它们互作比较，这些方法包括：演绎验证、自动验证、测试和进程代数

 为具体项目的软件选择过程提供有用信息

 提供了大量的练习、项目和连续性的实例，方便读者学习形式化方法并能够亲手使用这些工具

 介绍了支持形式化方法的数学原理

 对于该领域未来的研究方向，以及开发新方法和改进现有技术提出了有益的见解

作者简介

【作者简介】

Doron A. Peled 以色列巴依兰大学（BarIlan University）计算机科学系教授。主要研究领域为并发理论、形式化验证、形式化规约、编程语言语义、模型检验、有限自动机、软件测试、时序逻辑等。著有多部书籍和论文。

【译者简介】

王林章 南京大学计算机科学与技术系副教授、硕士生导师，南京大学计算机软件新技术国家重点实验室主任助理。主要研究方向为软件工程、新型软件测试方法、模型驱动软件测试与验证、自动化软件测试工具。目前面向本科生、研究生讲授软件工程、软件体系结构、软件测试等课程。

目录信息

出版者的话
中文版序
译者序
英文版序
前言
第1章　引言1
1.1　形式化方法2
1.2　开发与学习形式化方法3
1.3　使用形式化方法5
1.4　应用形式化方法6
1.5　本书概要7
第2章　预备知识8
2.1　集合表示法8
2.2　字符串和语言9
2.3　图10
2.4　计算复杂度和可计算性12
2.5　扩展阅读16
第3章　逻辑和定理证明17
3.1　一阶逻辑17
3.2　项17
3.2.1　赋值和解释18
3.2.2　多个论域上的结构19
3.3　一阶公式19
3.4　命题逻辑23
3.5　证明一阶逻辑公式24
3.5.1　正向推理25
3.5.2　反向推理26
3.6　证明系统的属性26
3.6.1　正确性27
3.6.2　完备性27
3.6.3　可判定性27
3.6.4　结构完备性28
3.7　证明命题逻辑属性28
3.8　一个实用的证明系统29
3.9　证明示例31
3.10　机器辅助证明37
3.11　机械化定理证明器39
3.12　扩展阅读39
第4章　软件系统建模40
4.1　顺序系统、并发系统及反应式系统41
4.2　状态42
4.3　状态空间43
4.4　转换系统44
4.5　转换的粒度47
4.6　为程序建模的例子48
4.6.1　整数除法48
4.6.2　计算组合数49
4.6.3　Eratosthenes筛法50
4.6.4　互斥52
4.7　非确定性转换53
4.8　将命题变量赋给状态54
4.9　合并状态空间55
4.10　线性视角56
4.11　分支视角57
4.12　公平性58
4.13　偏序视角61
4.13.1　一个银行系统的例子61
4.13.2　线性化和全局状态63
4.13.3　一个简单的例子64
4.13.4　偏序模型的应用65
4.14　形式化建模65
4.15　一个项目的建模67
4.16　扩展阅读68
第5章　形式化规约69
5.1　规约机制的属性69
5.2　线性时序逻辑70
5.3　公理化LTL74
5.4　LTL规约示例74
5.4.1　交通灯74
5.4.2　顺序程序的属性75
5.4.3　互斥76
5.4.4　公平性条件76
5.5　无限字上的自动机77
5.6　使用Büchi自动机作为规约79
5.7　确定性Büchi自动机80
5.8　其他规约机制81
5.9　复杂的规约83
5.10　规约的完整性83
5.11　扩展阅读84
第6章　自动验证85
6.1　状态空间搜索86
6.2　状态表示方法87
6.3　自动机结构体系88
6.4　合并Büchi自动机89
6.4.1　广义Büchi自动机90
6.4.2　将广义Büchi自动机转换为简单Büchi自动机91
6.5　Büchi自动机求补92
6.6　检验空集93
6.7　模型检验范例94
6.8　将LTL转换为自动机95
6.9　模型检验的复杂度100
6.10　表示公平性102
6.11　检验LTL规约102
6.12　安全属性103
6.13　状态空间爆炸问题104
6.14　模型检验的优点105
6.15　模型检验的缺点105
6.16　选择自动验证工具105
6.17　模型检验项目105
6.18　模型检验工具106
6.19　扩展阅读106
第7章　演绎式软件验证107
7.1　流程图程序的验证107
7.2　含数组变量的验证111
7.2.1　含数组变量赋值的问题112
7.2.2　修改证明系统112
7.3　完全正确性114
7.4　公理式程序验证117
7.4.1　赋值公理117
7.4.2　空语句公理117
7.4.3　左强化规则117
7.4.4　右弱化规则118
7.4.5　顺序组合规则118
7.4.6　if-then-else规则118
7.4.7　while规则118
7.4.8　begin-end规则119
7.4.9　示例：整数除法119
7.5　并发程序的验证121
7.6　演绎验证的优点124
7.7　演绎验证的缺点125
7.8　证明系统的正确性和完备性126
7.9　组合性127
7.10　演绎验证工具128
7.11　扩展阅读128
第8章　进程代数与等价关系129
8.1　进程代数130
8.2　通信系统的演算131
8.2.1　动作前缀131
8.2.2　选择132
8.2.3　并发组合132
8.2.4　限制符133
8.2.5　重标记133
8.2.6　等式定义133
8.2.7　agent 0135
8.2.8　传值agent135
8.3　示例：Dekker算法135
8.4　建模问题137
8.5　agent之间的等价性138
8.5.1　迹等价139
8.5.2　失败等价139
8.5.3　模拟等价140
8.5.4　互模拟和弱互模拟等价142
8.6　等价关系的层级142
8.7　用进程代数研究并发143
8.8　计算互模拟等价145
8.9　LOTOS147
8.10　进程代数工具148
8.11　扩展阅读148
第9章　软件测试150
9.1　审查和走查151
9.2　控制流覆盖准则152
9.2.1　语句覆盖153
9.2.2　边覆盖153
9.2.3　条件覆盖153
9.2.4　边/条件覆盖154
9.2.5　条件组合覆盖154
9.2.6　路径覆盖154
9.2.7　不同覆盖准则的比较155
9.2.8　循环覆盖155
9.3　数据流覆盖准则155
9.4　传播路径条件157
9.4.1　示例：GCD程序159
9.4.2　含有输入语句的路径160
9.5　等价类划分160
9.6　待测代码预处理160
9.7　检查测试套件161
9.8　组合性162
9.9　黑盒测试163
9.10　概率测试164
9.11　测试的优点165
9.12　测试的缺点166
9.13　测试工具166
9.14　扩展阅读166
第10章　组合形式化方法167
10.1　抽象167
10.2　组合测试与模型检验171
10.2.1　直接检验171
10.2.2　黑盒系统172
10.2.3　组合锁自动机172
10.2.4　黑盒死锁检测172
10.2.5　一致性测试173
10.2.6　检验重置的可靠性175
10.2.7　黑盒检验176
10.3　净室方法177
10.3.1　验证177
10.3.2　证明审查177
10.3.3　测试177
10.4　扩展阅读178
第11章　可视化179
11.1　在形式化方法中运用可视化179
11.2　消息序列图180
11.3　可视化流程图和状态机182
11.4　层次状态图184
11.4.1　层次化状态184
11.4.2　统一的出口和入口185
11.4.3　并发185
11.4.4　输入和输出185
11.5　程序文本的可视化186
11.6　Petri网186
11.7　可视化工具188
11.8　扩展阅读188
结束语189
参考文献191
· · · · · · (收起)

用户评价

这本书的行文风格简直是一场折磨，语言组织得过于学术化和冗长，仿佛作者是在撰写一篇博士论文，而不是一本面向工程师的实用手册。很多本应一句话说清的道理，非要用三段话、十几个从句来堆砌，让人在理解核心概念时需要花费大量的精力去梳理和提炼。我翻阅了很多章节，试图寻找一些可以直接应用到我们正在进行的项目中的快速解决方案或Checklist，但收获甚微。书中对各种模型和框架的介绍，更多是罗列其历史渊源和理论基础，对于如何在现代DevOps流水线中集成这些方法，介绍得极其模糊和蜻蜓点水。比如，它提到了某个著名的风险分析技术，但对于如何自动化这一过程，或者如何将分析结果反馈到CI/CD管道中，几乎没有提及。这使得这本书的实用价值大打折扣，它更像是一个理论的博物馆，而非一个实用的工具箱。阅读过程中，我多次感到挫败，觉得时间花在了理解晦涩的句子结构上，而不是真正吸收知识点上。

我对这本书的期待是它能提供一套系统性的、可扩展的质量保证体系框架，能够适应不同规模和不同技术栈的团队。然而，这本书给我的感觉更像是一系列独立专题论文的拼凑，各个章节之间的内在逻辑联系并不紧密。前一章还在大谈特谈形式化验证的严谨性，下一章立刻跳到了用户体验的度量，两者之间的桥梁搭建得非常生硬。我尤其关注了关于大规模分布式系统可靠性设计的部分，但发现这部分内容极其简略，几乎没有涉及微服务架构下的熔断、限流、幂等性设计等关键议题。作者似乎更偏爱那些成熟、经典、但在快速迭代的互联网行业中可能显得有些过时的技术栈。我需要的，是如何在混沌和快速变化的环境中构建韧性，这本书提供的哲学指导多于具体的工程实践指导。如果这是一本面向学术界读者的综述性著作，或许可以接受，但作为一本声称指导工程实践的书籍，其结构上的松散和侧重点的偏差，让它难以成为我案头的常备参考书。

这本书的封面设计倒是挺朴素的，拿到手上感觉挺扎实的，纸张的质感也不错，长时间阅读下来眼睛不太容易疲劳。我本来是冲着某个具体的软件工程理论来的，想看看作者是怎么把它融入到实际项目中的。结果发现，这本书的内容更像是一本宏观的导论，它花了大量的篇幅去探讨“为什么我们需要关注软件的质量”，而不是深入到具体的“如何实现高质量”。书中引用的案例大多是教科书式的标准案例，虽然清晰，但缺乏那种让人拍案叫绝的、来自于一线实战的“血淋淋”的教训和解决方案。对于一个已经有几年开发经验的工程师来说，这本书提供的新知非常有限，更像是对已掌握知识点的梳理和归纳，读起来有点像是在重温大学时的教材，知识点都在那里，但缺乏那种“aha!”的瞬间。我期待的是能看到一些不那么为人所知、但在业界被证明行之有效的新兴工具链或者敏捷开发中的质量保障新思路，这本书在这方面显得有些保守和传统。总体而言，作为入门级参考可以，但对于寻求突破和前沿技术的读者来说，深度和广度可能都不够令人满意。

这本书在图表和可视化方面做得实在是不够用心。在解释那些复杂的流程依赖关系或者故障传播路径时，如果能有一个清晰的、分层的流程图或状态转移图，理解起来会事半功倍。但遗憾的是，大部分复杂的概念都依赖于纯文字的描述，这极大地增加了读者的认知负荷。比如，书中描述的那个多层级的故障注入和恢复机制，我反复阅读了好几遍，才勉强在脑海中勾勒出一个模糊的轮廓，如果能配上一张详细的状态机图示，效果会完全不同。这种对可视化表达的忽视，在技术写作中是一个非常明显的短板，尤其是在讨论“系统性错误”这类需要清晰空间和时间概念的内容时。此外，书中引用的参考文献列表也显得有些陈旧，很多近五年的重要行业白皮书和顶会论文都没有被纳入讨论范围，这让我对其内容的“新颖性”和“前沿性”产生了深深的疑问。感觉这本书的编纂周期可能相当长，导致其内容在发布时就已经滞后于行业发展速度了。

从内容深度来看，这本书更像是对软件工程基础课程的一个“扩展阅读材料”，而不是一本深入研究特定领域专精的著作。它触及了测试、度量、风险管理等多个方面，但每一项都只是浅尝辄止，没有一个点能让人深入挖掘到可以动手实践的细节。我尝试寻找关于特定编程语言的最佳实践来提升代码质量的章节，但发现书中对语言特性的讨论几乎为零，所有的“可靠性”都抽象成了一种与技术细节无关的哲学层面。对于那些希望通过阅读来提升编码规范、掌握高级调试技巧或者学习如何编写具有高内聚低耦合特性的代码的初级和中级开发者来说，这本书提供的帮助微乎其微。它似乎更倾向于取悦那些制定战略和政策的管理者，而不是那些每天需要编写和维护代码的工程师。它的价值在于提供了一种自上而下的视角，但对于自下而上的技术积累和能力提升，这本书的贡献相当有限，读完后感觉知识结构没有得到实质性的巩固和强化。

总要把不喜欢的事情尽快做完，才能去做喜欢的事情，正如科研之于我。把不喜欢、不擅长的事情做完，才有成就感。把喜欢的、擅长的事情做好，才有幸福感。P.S. 书的确是好书，不可否认，不能以主观的喜好来代替客观的评判。

软件可靠性方法是一本非常经典的讲解软件形式化方法的书，书的作者Doron A. Peled不仅介绍了形式化方法所用到的逻辑、自动机理论等基础的数学知识，还深入的讨论了软件形式化常用到的推理验证、软件测试、模型检验等重要的软件形式化方法。

软件可靠性方法是一本非常经典的讲解软件形式化方法的书，书的作者Doron A. Peled不仅介绍了形式化方法所用到的逻辑、自动机理论等基础的数学知识，还深入的讨论了软件形式化常用到的推理验证、软件测试、模型检验等重要的软件形式化方法。

软件可靠性方法是一本非常经典的讲解软件形式化方法的书，书的作者Doron A. Peled不仅介绍了形式化方法所用到的逻辑、自动机理论等基础的数学知识，还深入的讨论了软件形式化常用到的推理验证、软件测试、模型检验等重要的软件形式化方法。

总要把不喜欢的事情尽快做完，才能去做喜欢的事情，正如科研之于我。把不喜欢、不擅长的事情做完，才有成就感。把喜欢的、擅长的事情做好，才有幸福感。P.S. 书的确是好书，不可否认，不能以主观的喜好来代替客观的评判。