软件可靠性方法

出版时间：2012-3  出版社：机械工业出版社  作者：（以色列）Doron A. Peled  译者：王林章 等  
Tag标签：无  

内容概要

　　【名人推荐】
　　我第一次翻开这本书时，立刻被这本书的覆盖范围之广所深深打动，它覆盖了规约和建模、演绎验证、模型检验、进程代数、程序测试、状态与消息序列图。除了对每个方法进行了相当深入的介绍以外，本书还讨论了应当在何时选取何种方法以及在选择这些方法时所必须做出的权衡。书中结合当前工具，使用很多具有挑战性的实例来说明各种技术。我还没看见过其他任何覆盖同样内容的书籍能达到如此的深度。
　　同时，本书描述了应用形式化方法的过程：从建模和规约开始，然后选择一个合适的验证技术，最后测试程序。这些知识在实践中是十分必要的，但是却很少在软件工程的课本里面出现。我确信这本书将会取得巨大的成功。我向所有对软件可靠性问题感兴趣的读者强烈推荐这本书。
　　—— Edmund M. Clarke教授
　　图灵奖获得者，卡内基-梅隆大学
　　【内容简介】
　　用于创建可靠软件的形式化方法一直处于不断的开发和改进之中。最近，人们对于形式化方法工具的重要组成有了更深入的理解，从软硬件开发业界逐渐接受可靠性工具这一点就可以体现出来。
　　本书介绍了各种能解决软件可靠性问题的方法。理想情况下，形式化方法应该用起来直观，学起来简洁、快速，对开发过程的影响微乎其微。本书对各种方法进行了比较，揭示了它们各自的优点和缺点，同时紧扣自动机理论和逻辑这两个主题。在尽可能减少背景知识介绍的前提下，本书向非专家读者描述了多种技术，并且针对软件工程领域的研究人员和专业人士介绍了一些高级技术。
　　本书主题和特点：
　　? 集中介绍目前常用的重要软件可靠性方法，并将它们互作比较，这些方法包括：演绎验证、自动验证、测试和进程代数
　　? 为具体项目的软件选择过程提供有用信息
　　? 提供了大量的练习、项目和连续性的实例，方便读者学习形式化方法并能够亲手使用这些工具
　　? 介绍了支持形式化方法的数学原理
　　? 对于该领域未来的研究方向，以及开发新方法和改进现有技术提出了有益的见解

作者简介

　　Doron A. Peled 以色列巴依兰大学（BarIlan
University）计算机科学系教授。主要研究领域为并发理论、形式化验证、形式化规约、编程语言语义、模型检验、有限自动机、软件测试、时序逻辑等。著有多部书籍和论文。
　　王林章
南京大学计算机科学与技术系副教授、硕士生导师，南京大学计算机软件新技术国家重点实验室主任助理。主要研究方向为软件工程、新型软件测试方法、模型驱动软件测试与验证、自动化软件测试工具。目前面向本科生、研究生讲授软件工程、软件体系结构、软件测试等课程。

书籍目录

出版者的话
中文版序　
译者序
英文版序
前言
第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　公理化LTL
　5.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　agent 0
　　8.2.8　传值agent
　8.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　LOTOS
　8.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　扩展阅读
结束语
参考文献

章节摘录

版权页：插图：早期的形式化方法是基于文本的，具体包括对系统的形式化表示、系统属性的规约以及与工具、测试和验证结果的交互过程。近年来，研究人员和从业人员开始意识到对软件进行可视化表示将会极大地提高软件开发效率。在许多情况下，人们通过对代码的可视化表示的观察，能够得到一些新的信息，如不同的程序对象以及它们之间的关联、控制流、通信模式等。这种直观的理解是无法通过一行一行地阅读代码获得的。使用可视化表示法的趋势在软件开发方法学（如UML[46]）所使用的多种图中都得到了最好的反映。这些不同种类的图可以用于描述系统的体系结构、系统中包含的不同进程或对象、进程或对象的交互、进程或对象的转换、典型和异常的执行、系统模块之间的关联等等。本章将讨论如何通过可视化表示来给形式化方法带来益处。可视化系统所带来的好处是我们可以把呆板的语法映射成图形化对象之间的关系。例如，考虑一下，在描述自动机时，使用状态转换图或者使用包括初始及结束状态的状态转换表，哪个更易于接受？由此可见，可视化的表示在演示动态过程时有着独特的优势。再如，在表示模型检验中的某个反例时，一张标记了执行路径的流程图显然要比只是简单地列出其所执行过的代码要更加直观。11.1 在形式化方法中运用可视化我们已经见过了一些既可以用文本化也可以用图形化描述的符号。其一是自动机，它通过文本化或图形化的方式来描述系统的组成成分。其二是流程图，它使用图的形式展示程序。这些示例展示了基于文字和基于图形的两种不同表示方法。这两种表示方法之间的转换都被形式化地定义过。形式化方法的工具通常允许用户与图形化的表示进行交互。对象的添加、删除、复制、大小调整、重定位、改变标签等都已经基本上成为了图形化表示方法中的标准操作。由于互联网的广泛使用，一些常见的选择或者更新操作在屏幕上都是以同样的感官展现。而这些带给用户的好处就是可以花费更少的时间来熟悉一个新的系统。由于目前计算机对文本数据的处理仍优于对图形化数据的处理，所以基于可视化表示的工具通常需要在图形化和文本化描述形式之间做转换。基于文本的表示通常是存储在文本文件里面的。当工具需要使用这个表示的时候，需要先读入这个文本文件，然后生成图形化的表示，最终显示出来。当用户通过和工具之间的交互改变了图形化表示的时候，那么工具就要对应地修改该文本表示。

编辑推荐

《软件可靠性方法》编辑推荐：集中介绍目前常用的重要软件可靠性方法，并将它们互作比较，这些方法包括：演绎验证、自动验证、测试和进程代数，为具体项目的软件选择过程提供有用信息，提供了大量的练习、项目和连续性的实例，方便读者学习形式化方法并能够亲手使用这些工具介绍了支持形式化方法的数学原理，对于该领域未来的研究方向，以及开发新方法和改进现有技术提出了有益的见解。

用户评论 (总计1条)

•   值得购买!!!! 有兴趣的可以买