软件可靠性方法 7111365534, 9787111365532

封面\n书名\n版权\n前言\n目录\n第1章  引言\n1.1形式化方法\n1.2开发与学习形式化方法\n1.3使用形式化方法\n1.4应用形式化方法\n1.5本书概要\n第2章  预备知识\n2.1集合表示法\n2.2字符串和语言\n2.3图\n2.4计算复杂度和可计算性\n2.5扩展阅读\n第3章  逻辑和定理证明\n3.1一阶逻辑\n3.2项\n3.2.1赋值和解释\n3.2.2多个论域上的结构\n3.3一阶公式\n3.4命题逻辑\n3.5证明一阶逻辑公式\n3.5.1正向推理\n3.5.2反向推理\n3.6证明系统的属性\n3.6.1正确性\n3.6.2完备性\n3.6.3可判定性\n3.6.4结构完备性\n3.7证明命题逻辑属性\n3.8一个实用的证明系统\n3.9证明示例\n3.10机器辅助证明\n3.11机械化定理证明器\n3.12扩展阅读\n第4章  软件系统建模\n4.1顺序系统、并发系统及反应式系统\n4.2状态\n4.3状态空间\n4.4转换系统\n4.5转换的粒度\n4.6为程序建模的例子\n4.6.1整数除法\n4.6.2计算组合数\n4.6.3  Eratosthenes筛法\n4.6.4互斥\n4.7非确定性转换\n4.8将命题变量赋给状态\n4.9合并状态空间\n4.10线性视角\n4.11分支视角\n4.12公平性\n4.13偏序视角\n4.13.1一个银行系统的例子\n4.13.2线性化和全局状态\n4.13.3一个简单的例子\n4.13.4偏序模型的应用\n4.14形式化建模\n4.15一个项目的建模\n4.16扩展阅读\n第5章  形式化规约\n5.1规约机制的属性\n5.2线性时序逻辑\n5.3公理化LTL\n5.4  LTL规约示例\n5.4.1交通灯\n5.4.2顺序程序的属性\n5.4.3互斥\n5.4.4公平性条件\n5.5无限字上的自动机\n5.6使用Buchi自动机作为规约\n5.7确定性Buchi自动机\n5.8其他规约机制\n5.9复杂的规约\n5.10规约的完整性\n5.11扩展阅读\n第6章  自动验证\n6.1状态空间搜索\n6.2状态表示方法\n6.3自动机结构体系\n6.4合并Buchi自动机\n6.4.1广义Buchi自动机\n6.4.2将广义Buchi自动机转换为简单Buchi自动机\n6.5  Buchi自动机求补\n6.6检验空集\n6.7模型检验范例\n6.8将LTL转换为自动机\n6.9模型检验的复杂度\n6.10表示公平性\n6.11检验LTL规约\n6.12安全属性\n6.13状态空间爆炸问题\n6.14模型检验的优点\n6.15模型检验的缺点\n6.16选择自动验证工具\n6.17模型检验项目\n6.18模型检验工具\n6.19扩展阅读\n第7章  演绎式软件验证\n7.1流程图程序的验证\n7.2含数组变量的验证\n7.2.1含数组变量赋值的问题\n7.2.2修改证明系统\n7.3完全正确性\n7.4公理式程序验证\n7.4.1赋值公理\n7.4.2空语句公理\n7.4.3左强化规则\n7.4.4右弱化规则\n7.4.5顺序组合规则\n7.4.6  if-then-else规则\n7.4.7 while规则\n7.4.8  begin-end规则\n7.4.9示例：整数除法\n7.5并发程序的验证\n7.6演绎验证的优点\n7.7演绎验证的缺点\n7.8证明系统的正确性和完备性\n7.9组合性\n7.10演绎验证工具\n7.11扩展阅读\n第8章  进程代数与等价关系\n8.1进程代数\n8.2通信系统的演算\n8.2.1动作前缀\n8.2.2选择\n8.2.3并发组合\n8.2.4限制符\n8.2.5重标记\n8.2.6等式定义\n8.2.7  agent 0\n8.2.8传值agent\n8.3示例：Dekker算法\n8.4建模问题\n8.5  agent之间的等价性\n8.5.1迹等价\n8.5.2失败等价\n8.5.3模拟等价\n8.5.4互模拟和弱互模拟等价\n8.6等价关系的层级\n8.7用进程代数研究并发\n8.8计算互模拟等价\n8.9  LOTOS\n8.10进程代数工具\n8.11扩展阅读\n第9章  软件测试\n9.1审查和走查\n9.2控制流覆盖准则\n9.2.1语句覆盖\n9.2.2边覆盖\n9.2.3条件覆盖\n9.2.4边/条件覆盖\n9.2.5条件组合覆盖\n9.2.6路径覆盖\n9.2.7不同覆盖准则的比较\n9.2.8循环覆盖\n9.3数据流覆盖准则\n9.4传播路径条件\n9.4.1示例：GCD程序\n9.4.2含有输入语句的路径\n9.5等价类划分\n9.6待测代码预处理\n9.7检查测试套件\n9.8组合性\n9.9黑盒测试\n9.10概率测试\n9.11测试的优点\n9.12测试的缺点\n9.13测试工具\n9.14扩展阅读\n第10章  组合形式化方法\n10.1抽象\n10.2组合测试与模型检验\n10.2.1直接检验\n10.2.2黑盒系统\n10.2.3组合锁自动机\n10.2.4黑盒死锁检测\n10.2.5一致性测试\n10.2.6检验重置的可靠性\n10.2.7黑盒检验\n10.3净室方法\n10.3.1验证\n10.3.2证明审查\n10.3.3测试\n10.4扩展阅读\n第11章  可视化\n11.1在形式化方法中运用可视化\n11.2消息序列图\n11.3可视化流程图和状态机\n11.4层次状态图\n11.4.1层次化状态\n11.4.2统一的出口和入口\n11.4.3并发\n11.4.4输入和输出\n11.5程序文本的可视化\n11.6  Petri网\n11.7可视化工具\n11.8扩展阅读\n结束语\n参考文献