本书通过大量的形式化表示和技术，向读者提供了各种用于提高软件可靠性的形式化方法，包括演绎验证、自动验证、测试以及进程代数。紧紧围绕逻辑和自动机理论这条主线，书中比较了这些方法的不同之处，并讨论了它们的优点和缺点。
书中包含一些在多个章节中使用的、具有连续性的实例，有利于读者通过跟踪这些实例来了解不同形式化方法的优缺点。本书还包括大量的练习和项目，可以使用软件可靠性工具来完成。
本书适合于从事软件开发的广大读者，尤其适合高年级本科生软件可靠性课程和硕士阶段软件工程课程使用。
软件可靠性方法
Software Reliability Methods
（以）Doron A. Peled 著
王林章 卜磊 陈鑫 张天 赵建华 李宣东 译
用于创建可靠软件的形式化方法一直处于不断的开发和改进之中。最近，人们对于形式化方法工具的重要组成有了更深入的理解，从软硬件开发业界逐渐接受可靠性工具这一点就可以体现出来。
本书介绍了各种能解决软件可靠性问题的方法。理想情况下，形式化方法应该用起来直观，学起来简洁、快速，对开发过程的影响微乎其微。本书对各种方法进行了比较，揭示了它们各自的优点和缺点，同时紧扣自动机理论和逻辑这两个主题。在尽可能减少背景知识介绍的前提下，本书向非专家读者描述了多种技术，并且针对软件工程领域的研究人员和专业人士介绍了一些高级技术。
本书特点
集中介绍目前常用的重要软件可靠性方法，并将它们互作比较，这些方法包括：演绎验证、自动验证、测试和进程代数
为具体项目的软件选择过程提供有用信息
提供了大量的练习、项目和连续性的实例，方便读者学习形式化方法并能够亲手使用这些工具
介绍了支持形式化方法的数学原理
对于该领域未来的研究方向，以及开发新方法和改进现有技术提出了有益的见解
前
作者简介
Doron A. Peled
以色列巴依兰大学（BarIlan University）计算机科学系教授。主要研究领域为并发理论、形式化验证、形式化规约、编程语言语义、模型检验、有限自动机、软件测试、时序逻辑等。著有多部书籍和论文。
译者简介
王林章
南京大学计算机科学与技术系副教授、硕士生导师，南京大学计算机软件新技术国家重点实验室主任助理。主要研究方向为软件工程、新型软件测试方法、模型驱动软件测试与验证、自动化软件测试工具。目前面向本科生、研究生讲授软件工程、软件体系结构、软件测试等课程。
后：
我第一次翻开这本书时，立刻被这本书的覆盖范围之广所深深打动，它覆盖了规约和建模、演绎验证、模型检验、进程代数、程序测试、状态与消息序列图。除了对每个方法进行了相当深入的介绍以外，本书还讨论了应当在何时选取何种方法以及在选择这些方法时所必须做出的权衡。书中结合当前工具，使用很多具有挑战性的实例来说明各种技术。我还没看见过其他任何覆盖同样内容的书籍能达到如此的深度。
同时，本书描述了应用形式化方法的过程：从建模和规约开始，然后选择一个合适的验证技术，最后测试程序。这些知识在实践中是十分必要的，但是却很少在软件工程的课本里面出现。我确信这本书将会取得巨大的成功。我向所有对软件可靠性问题感兴趣的读者强烈推荐这本书。
—— Edmund M. Clarke教授
图灵奖获得者，卡内基-梅隆大学
许多书籍描述了如何通过应用形式化方法来提高软件的质量。然而，大多数书籍都是围绕着某个特定的方法，并将该方法作为软件可靠性问题的推荐解决方案。本书通过大量的形式化符号表示法和技术，向读者呈现了形式化方法更加全面的描述。书中将会比较它们之间的不同之处，并讨论它们的优点与缺点。
形式化方法的主要挑战之一在于怎样将研究人员开发出的技术传播到软件开发社区中去。最近一段时间，我们似乎开始对形式化方法工具的重要组成部分有了更好的理解。这表现为此类工具越来越多地被软、硬件开发业界所接受。理想情况下，形式化方法必须可以被直观地使用（最好是使用图形化界面），不要求使用者花费大量的学习时间，并且在开发过程中只产生比较小的额外开销。相比于10年或20年前，形式化方法更容易被人们所接受，这在硬件领域尤为显著。然而，不同的方法之间仍然存在激烈的争论。
本书重点是通过一系列技术来讲述形式化方法的主要原理。有很多在撰写本书时已有的先进技术没有包括在本书中。这些先进的技术涉及实时系统和混成系统、描述规约的形式化体系，以及一些专用的数据结构，比如二元决策图。本书没有包含这些特定的技术，但这并不意味着本书中的方法优于它们，而是因为本书描述的算法和方法已经应用于目前最先进的软件可靠性工具中了。挑选出来这些方法仅仅是想以举一反三的方式来表现形式化方法这一主题。然而，挑选时总是不可避免地倾向于选择和我的研究方向比较接近的主题。贯穿本书的主线是逻辑和自动机理论。有兴趣的读者可以在相关章节后列出的其他书籍和研究论文中找到这些高级方法的细节。
如果没有直接使用相关工具的实际经验，对形式化方法的学习就是不完整的。本书包含了大量的练习和项目，可以使用软件可靠性工具来完成它们。书中还有一些在多个章节中使用的、具有连续性的实例。学习形式化方法并且了解其优点和缺陷的一个有效方法是跟踪理解这些跨章节的实例。在一些情况下，后面的章节会详述某个在前面章节的练习部分提到的连续性实例。这样做的另一个目的是帮助读者检查对前面章节练习的解答（而不是仅仅提供一个明确的答案）。我们鼓励读者去检查所获得的关于这些例子的直觉感受可否帮助改进他们对之前练习的解答。
书中提供的绝大部分练习和项目可以选择某个工具来完成。尽管一些软件可靠性工具要求不菲的许可费用，但是很多工具允许出于非盈利目的免费使用。使用这些工具通常需要从这些工具的万维网页下载并按照网页上的指示进行安装。相关章节后面列出了一些工具和相应网页。需要注意的是，即使有些工具不需要取得许可证就可以使用，它们也常常要求使用者向工具的开发者发送一份信件，同意遵守工具的使用条款。在许多情况下，这些条款限定工具只能用于学术目的，并且开发者不对因使用工具而可能造成的损害负责。由于网页和网址往往会变更，同时也因为新的工具不断被开发出来替代已有的工具，因此我不能保证书中列出的网页信息一直有效。此外，本书不能够保证这些工具可以在任何环境下都正常工作。
不同的团体对形式化方法有不同的兴趣，当然不可能写出一本对项目经理、软件开发人员、质量保证团队和研究人员具有相同吸引力的书，但是我仍然尝试着在书中加入令每个读者群中的成员都感兴趣的内容。因此，读者在阅读的时候可以跳过那些理论性或技术性太强的章节。应当指出的是，本书的重点主要是技术，而不是方法学。
本书在描述一些形式化方法的同时还给出了相应的算法，理解这些算法对于运用这些方法并不是必不可少的，但是理解它们可以更加深入地了解这些方法的工作原理。本书省略了大多数和书中的形式化方法相关的数学证明，但有时会包含简略的证明，以便增加读者的直观理解。
作者在此感谢下面这些参与和本书相关的启发性讨论并提出有益建议的人员：Nina Amla、Christel Baier、David Basin、Shai Ben-David、Roderick Bloem、Glenn Bruns、Ed Clarke、Dennis Dams、Xiaoqun Du、Kousha Etessami、Amy Felty、Elsa Gunter、Doug Howe、Orna Kupferman、Bart Knaack、Bob Kurshan、Bengt Jonsson、Leonid Libkin、Anca Muscholl、Kedar Namjoshi、Wojciech Penczek、Kavita Ravi、Natarajan Shankar、Natasha Sharygina、Marian Srenby、Richard Tefler、Wolfgang Thomas、Moshe Vardi、Igor Walukiewicz、Thomas Wilke、Mihalis Yannakakis和Lenore Zuck。事实上，写这本书的最大收获之一是有机会从实践者和专家就某些特定主题给出的建议和评论中进一步学习。
我并不是第一个引用刘易斯·卡洛尔（Lewis Carroll）的探险小说中的词句的。但是，鲜为人知的是Charles Lutwidge Dodgson（笔名是Lewis Carroll）是一个研究逻辑可视化表示的数学家。他的“biliteral”（两字母）和“triliteral”（三字母）图是卡诺图的前身。卡诺图能够用一种易教易学的方式来表示逻辑，这也是很多形式化方法的最新研究趋势。
Doron Peled
2001年3月于新泽西州莫雷山
本书中所引《Alice’s Adventures in Wonderland》中词句的中文翻译引自陈复庵先生所翻译的《阿丽思漫游奇境记》（中国对外翻译出版公司 1987年版），所引《Through the Looking Glass》中词句的中文翻译引自许季鸿先生所翻译的《艾丽丝镜中奇遇记》（文化艺术出版社 1986年版）。本书译者将书中主人公名译成“爱丽丝”。——译者注
计算机\软件工程
这本书是软件方法技术的介绍，是学习各种用于增强软件可靠性的方法的宝贵资源，是形式化方法技术的指南，是大学一学期课程的基本教材。
用于创建可靠软件的形式化方法一直处于不断的开发和改进之中。最近，人们对于形式化方法工具的重要组成有了更深入的理解，从软硬件开发业界逐渐接受可靠性工具这一点就可以体现出来。
本书介绍了各种能解决软件可靠性问题的方法。理想中，形式化方法应该用起来直观，学起来简洁、快速，对开发过程的影响微乎其微。本书对各种方法进行了比较，揭示了它们各自的优点和缺点，同时紧扣自动机理论和逻辑这两个主题。在尽可能减少背景知识介绍的前提下，本书向非专家读者描述了多种技术，并且针对软件工程领域的研究人员和专业人士介绍了一些高级技术。
本书主题和特点：
n 集中介绍目前常用的重要软件可靠性方法，并将它们互作比较，这些方法包括：演绎验证、自动验证、测试和进程代数
n 为具体项目的软件选择过程提供有用信息
n 提供了大量的练习、项目和连续性的实例，方便读者学习形式化方法并能够亲手使用这些工具
n 介绍了支持形式化方法的数学原理
n 对于该领域未来的研究方向，以及开发新方法和改进现有技术提出了有益的见解
（以色列）Doron A. Peled 著：Doron A. Peled 以色列巴依兰大学（Bar Ilan University）计算机科学系教授。主要研究领域为：并发理论，形式化验证，形式化规约，编程语言语义，模型检验，有限自动机，软件测试，时序逻辑等。著有多部书籍和论文。
王林章 等译：暂无简介
进入21世纪以来，“高可信软件”先后被美国、欧盟列为优先资助的研究方向，我国科技部和国家自然科学基金委员会也在2007年分别为其设立了重点项目和重大研究计划，由此广泛推动了国内高校和科研单位在相关领域的研究工作。译者所在的南京大学软件工程组长期以来一直在开展与可信软件方法和技术相关的教学和研究工作，Doron A.Peled的《Software Reliability Methods》近年来一直被我们用做研究生的入门教材，是进入我们研究组的研究生必读的书籍。该书围绕软件可靠性较为全面、系统地介绍了相关方法和技术，深入浅出、通俗易懂。该书还受到了图灵奖获得者E.Clarke的大力推荐，作者本人在相关领域也很有建树。
2010年12月底，我与来访的机械工业出版社编辑姚蕾女士交流时，她了解到我们在用这本书，建议我们将它翻译成中文，以便让更多的国内读者能够深入理解作者的观点以及书中介绍的方法，从而在研究与实践中放手尝试。我们接受了她的建议，从2011年1月初开始着手翻译。参与本书翻译工作的主要是南京大学计算机软件新技术国家重点实验室、计算机科学与技术系软件工程组的老师和学生，分工情况如下：王林章（第9，10章、结束语）、卜磊（第5，6章）、陈鑫（第7，8章）、张天（第4，11章）、赵建华（第1，2，3章），王林章、李宣东对全书译稿进行了统稿、审校和修改。在翻译过程中得到研究生崔展齐、陈华杰、丁文旭、姜鹏、李游、李袁奎、柳溪、潘敏学、陶永晶、王寒非、邢雨辰、叶楠、张琦、周筱羽等的帮助，在此对他（她）们的辛勤劳动表示感谢。也感谢编辑王春华女士、夏平女士为本书所做的大量工作以及耐心等待。
尽管本书的翻译工作前后历时一年，但这是在大家繁忙的教学、科研以及各项服务工作之余完成的，所以仍感到时间紧张，有些内容的翻译表达仍不够理想。我们采用自己的研究方法来理解原书内容，对原文中我们认为表达错误或不确切的地方，也通过注释进行说明。限于我们的水平，中文表达难免有不当之处，在此敬请读者批评指正。如发现文字错误，请发邮件给王林章（lzwang@nju.edu.cn）。
王林章
2011年12月31日
出版者的话
中文版序
译者序
英文版序
前言
第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
