软件可靠性方法

出版者的话中文版序译者序英文版序前言第1章　引言1.1　形式化方法1.2　开发与学习形式化方法1.3　使用形式化方法1.4　应用形式化方法1.5　本书概要第2章　预备知识2.1　集合表示法2.2　字符串和语言2.3　图2.4　计算复杂度和可计算性2.5　扩展阅读第3章　逻辑和定理证明3.1　一阶逻辑3.2　项3.2.1　赋值和解释3.2.2　多个论域上的结构3.3　一阶公式3.4　命题逻辑3.5　证明一阶逻辑公式3.5.1　正向推理3.5.2　反向推理3.6　证明系统的属性3.6.1　正确性3.6.2　完备性3.6.3　可判定性3.6.4　结构完备性3.7　证明命题逻辑属性3.8　一个实用的证明系统3.9　证明示例3.10　机器辅助证明3.11　机械化定理证明器3.12　扩展阅读第4章　软件系统建模4.1　顺序系统、并发系统及反应式系统4.2　状态4.3　状态空间4.4　转换系统4.5　转换的粒度4.6　为程序建模的例子4.6.1　整数除法4.6.2　计算组合数4.6.3　Eratosthenes筛法4.6.4　互斥4.7　非确定性转换4.8　将命题变量赋给状态4.9　合并状态空间4.10　线性视角4.11　分支视角4.12　公平性4.13　偏序视角4.13.1　一个银行系统的例子4.13.2　线性化和全局状态4.13.3　一个简单的例子4.13.4　偏序模型的应用4.14　形式化建模4.15　一个项目的建模4.16　扩展阅读第5章　形式化规约5.1　规约机制的属性5.2　线性时序逻辑5.3　公理化LTL5.4　LTL规约示例5.4.1　交通灯5.4.2　顺序程序的属性5.4.3　互斥5.4.4　公平性条件5.5　无限字上的自动机5.6　使用Büchi自动机作为规约5.7　确定性Büchi自动机5.8　其他规约机制5.9　复杂的规约5.10　规约的完整性5.11　扩展阅读第6章　自动验证6.1　状态空间搜索6.2　状态表示方法6.3　自动机结构体系6.4　合并Büchi自动机6.4.1　广义Büchi自动机6.4.2　将广义Büchi自动机转换为简单Büchi自动机6.5　Büchi自动机求补6.6　检验空集6.7　模型检验范例6.8　将LTL转换为自动机6.9　模型检验的复杂度6.10　表示公平性6.11　检验LTL规约6.12　安全属性6.13　状态空间爆炸问题6.14　模型检验的优点6.15　模型检验的缺点6.16　选择自动验证工具6.17　模型检验项目6.18　模型检验工具6.19　扩展阅读第7章　演绎式软件验证7.1　流程图程序的验证7.2　含数组变量的验证7.2.1　含数组变量赋值的问题7.2.2　修改证明系统7.3　完全正确性7.4　公理式程序验证7.4.1　赋值公理7.4.2　空语句公理7.4.3　左强化规则7.4.4　右弱化规则7.4.5　顺序组合规则7.4.6　if-then-else规则7.4.7　while规则7.4.8　begin-end规则7.4.9　示例：整数除法7.5　并发程序的验证7.6　演绎验证的优点7.7　演绎验证的缺点7.8　证明系统的正确性和完备性7.9　组合性7.10　演绎验证工具7.11　扩展阅读第8章　进程代数与等价关系8.1　进程代数8.2　通信系统的演算8.2.1　动作前缀8.2.2　选择8.2.3　并发组合8.2.4　限制符8.2.5　重标记8.2.6　等式定义8.2.7　agent8.2.8　传值agent8.3　示例：Dekker算法8.4　建模问题8.5　agent之间的等价性8.5.1　迹等价8.5.2　失败等价8.5.3　模拟等价8.5.4　互模拟和弱互模拟等价8.6　等价关系的层级8.7　用进程代数研究并发8.8　计算互模拟等价8.9　LOTOS8.10　进程代数工具8.11　扩展阅读第9章　软件测试9.1　审查和走查9.2　控制流覆盖准则9.2.1　语句覆盖9.2.2　边覆盖9.2.3　条件覆盖9.2.4　边/条件覆盖9.2.5　条件组合覆盖9.2.6　路径覆盖9.2.7　不同覆盖准则的比较9.2.8　循环覆盖9.3　数据流覆盖准则9.4　传播路径条件9.4.1　示例：GCD程序9.4.2　含有输入语句的路径9.5　等价类划分9.6　待测代码预处理9.7　检查测试套件9.8　组合性9.9　黑盒测试9.10　概率测试9.11　测试的优点9.12　测试的缺点9.13　测试工具9.14　扩展阅读第10章　组合形式化方法10.1　抽象10.2　组合测试与模型检验10.2.1　直接检验10.2.2　黑盒系统10.2.3　组合锁自动机10.2.4　黑盒死锁检测10.2.5　一致性测试10.2.6　检验重置的可靠性10.2.7　黑盒检验10.3　净室方法10.3.1　验证10.3.2　证明审查10.3.3　测试10.4　扩展阅读第11章　可视化11.1　在形式化方法中运用可视化11.2　消息序列图11.3　可视化流程图和状态机11.4　层次状态图11.4.1　层次化状态11.4.2　统一的出口和入口11.4.3　并发11.4.4　输入和输出11.5　程序文本的可视化11.6　Petri网11.7　可视化工具11.8　扩展阅读结束语参考文献191

《软件可靠性方法》通过大量的形式化表示和技术，向读者提供了各种用于提高软件可靠性的形式化方法，包括演绎验证、自动验证、测试以及进程代数。书中紧紧围绕逻辑和自动机理论这条主线，比较了各种方法的不同之处，并讨论了它们的优缺点。　　书中包含一些在多个章节中使用的、具有连续性的实例，有利于读者通过跟踪这些实例来了解不同形式化方法的优缺点。本书还包括大量的练习和项目，可以使用软件可靠性工具来完成。　　本书适用于从事软件开发的广大读者，尤其适合作为高年级本科生和硕士生的教材和参考书。