中国年鉴信息网--中国规模最大、实力最强的研究报告提供商!您好,欢迎来到中国年鉴信息网! [登录] [注册] 我的购物车 我的订单
首 页
中国年鉴
研究报告
省市统计
中国名录
省市年鉴
地方志
社会经济
古籍文献
行业数据
软件可靠性方法
2012-05-23文字显示[ ]
[图书名称]:软件可靠性方法
[关键文字]:软件,可靠性,方法
[书刊号]:
[图书作者]:机械工业出版社
[出版日期]:2016年6月
[图书价格]:¥45.00
[优 惠 价]:¥45.00
[传真订购]:010-58697500
[咨询电话]:010-58697871 58697872
[值班手机]:13801017046
本书相关年份
软件可靠性方法 
     查看详细..
           
详细内容:  

    用于创建可靠软件的形式化方法一直处于不断的开发和改进之中。最近,人们对于形式化方法工具的重要组成有了更深入的理解,从软硬件开发业界逐渐接受可靠性工具这一点就可以体现出来。
    本书介绍了各种能解决软件可靠性问题的方法。理想情况下,形式化方法应该用起来直观,学起来简洁、快速,对开发过程的影响微乎其微。本书对各种方法进行了比较,揭示了它们各自的优点和缺点,同时紧扣自动机理论和逻辑这两个主题。在尽可能减少背景知识介绍的前提下,本书向非专家读者描述了多种技术,并且针对软件工程领域的研究人员和专业人士介绍了一些高级技术。
    本书特点
    集中介绍目前常用的重要软件可靠性方法,并将它们互作比较,这些方法包括:演绎验证、自动验证、测试和进程代数
为具体项目的软件选择过程提供有用信息
    提供了大量的练习、项目和连续性的实例,方便读者学习形式化方法并能够亲手使用这些工具
    介绍了支持形式化方法的数学原理
对于该领域未来的研究方向,以及开发新方法和改进现有技术提出了有益的见解

出版者的话
中文版序
译者序
英文版序
前言
第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

中国年鉴
研究报告
省市统计
中国名录
省市年鉴
地方志
社会经济
行业数据
古籍文献
友情链接:中国统计年鉴2013|中国2010年人口普查资料

中国年鉴信息网 版权所有 @1997-2013

电话:010-58697871 58697872 传真:010-58697500

Mail:chinayearbook@vip.sina.com 地址:北京朝阳区东三环中路39号建外SOHO12号楼2006室