本书从软件实际开发过程出发，将形式化技术应用于每个开发阶段，系统地介绍了基于B方法完成软件形式化开发的模式、过程、技术和方法，其中包括UML模型图到B方法形式规约的比较全面的转换方法，实现形式规约的精化过程，形式化B方法的验证技术，从UML形式化规约的逐步精化的规范与方法问题，整个规约、精化直到代码生产阶段的模型形式化验证及自动化，基于B方法的面向对象软件体系结构的形式化方法。通过该书的介绍使得学习者真正体会到如何应用形式化技术解决实际软件开发技术问题。基于形式化方法的高可信软件的开发基本走出实验室，满足高可信软件开发的需要。

　　崔梦天，教授，博士后，硕士生导师，四川省学术和技术带头人后备，获国家留学基金委资助。主要从事可信软件和优化算法的教学与科研工作。在《计算机学报》、《系统科学与电子技术》等刊物发表学术论文30余篇，出版专著1部。主持国家自然科学基金项目、中国博士后科学基金项目等课题多项。担任国家自然科学基金项目、四川省科技进步奖、四川省科技计划项目等评审专家以及国内外部分学术期刊评审专家。

第1章 绪论
1．1 研究背景
1．2 研究的意义
1．3 国内外研究现状及发展动态分析
1．4 本书的研究工作及现状分析
第2章 相关技术理论
2．1 形式化方法理论
2．1．1 形式规约
2．1．2 形式验证
2．2 B方法及相关技术简介
2．2．1 基本概念
2．2．2 广义代换和B抽象机
2．2．3 精化
2．2．4 B方法的优越性
2．3 UML统一建模语言
2．3．1 统一建模语言介绍
2．3．2 UML的内容及建模机制
2．3．3 类
2．3．4 关联
2．3．5 泛化
2．3．6 UML主要存在的问题与不足
2．4 依赖性分析理论
2．4．1 程序流图
2．4．2 控制依赖
2．4．3 数据依赖
2．4．4 程序依赖图
2．4．5 系统依赖图
2．5 程序切片技术
2．5．1 切片的定义
2．5．2 切片技术的分类
2．5．3 程序切片准则
2．6 本章小结
第3章 形式化B方法的软件开发
3．1 用B方法开发软件系统的过程
3．1．1 初始规范说明的开发
3．1．2 设计／精化
3．1．3 生成可执行代码
3．2 B方法使用的工具
3．2．1 ProB工具介绍
3．2．2 AtelierB的用法
3．2．3 抽象机实例
3．3 基于B方法的软件需求形式化过程
3．3．1 软件模型的实现过程
3．3．2 软件需求的形式化模型
3．3．3 软件需求的原型模型的实现
3．4 本章小结
第4章 形式化B方法与UML转换方法
4．1 UML和B方法概述
4．2 UML类图到B方法形式规约的转换
4．2．1 UML类图模型映射到B机器系统的基本方法和过程
4．2．2 类
4．2．3 操作
4．2．4 关联
4．2．5 泛化
4．2．6 类图
4．3 UML状态机到B模型的转换
4．3．1 UML状态机
4．3．2 B方法和B模型
4．3．3 UM状态图模型到B模型的具体的转换
4．4 UML活动图到B形式化规约的转换
4．5 UML顺序图到B形式化规约的转换
4．5．1 顺序图简介
4．5．2 UML中顺序图的B方法描述
4．5．3 举例
4．6 UML用例图到B的形式化转换
4．6．1 参与者
……
第5章 基于B技术的软件体系结构方法
第6章 实例分析
第7章 软件过程改进及软件过程集成
第8章 软件快速开发平台设计
第9章 过程模型在平台上实现的关键技术
主要参考文献
索引