软件可靠性方法

图书标准信息

• 作者 Doron A.Peled 著；王林章 译
• 出版社 机械工业出版社
• 出版时间 2012-03
• 版次 1
• ISBN 9787111365532
• 定价 45.00元
• 装帧 平装
• 开本 16开
• 纸张 胶版纸
• 页数 196页
• 正文语种 简体中文，英语
• 丛书 计算机科学丛书

【内容简介】

《软件可靠性方法》通过大量的形式化表示和技术，向读者提供了各种用于提高软件可靠性的形式化方法，包括演绎验证、自动验证、测试以及进程代数。书中紧紧围绕逻辑和自动机理论这条主线，比较了各种方法的不同之处，并讨论了它们的优缺点。

书中包含一些在多个章节中使用的、具有连续性的实例，有利于读者通过跟踪这些实例来了解不同形式化方法的优缺点。本书还包括大量的练习和项目，可以使用软件可靠性工具来完成。

本书适用于从事软件开发的广大读者，尤其适合作为高年级本科生和硕士生的教材和参考书。

【作者简介】

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

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

【目录】

出版者的话

中文版序

译者序

英文版序

前言

第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.3Eratosthenes筛法

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.4LTL规约示例

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.5Bü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.6if-then-else规则

7.4.7while规则

7.4.8begin-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.7agent

8.2.8传值agent

8.3示例：Dekker算法

8.4建模问题

8.5agent之间的等价性

8.5.1迹等价

8.5.2失败等价

8.5.3模拟等价

8.5.4互模拟和弱互模拟等价

8.6等价关系的层级

8.7用进程代数研究并发

8.8计算互模拟等价

8.9LOTOS

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.6Petri网

11.7可视化工具

11.8扩展阅读

结束语

参考文献191"