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