本書從軟件實際開發(fā)過程出發(fā),將形式化技術應用于每個開發(fā)階段,系統(tǒng)地介紹了基于B方法完成軟件形式化開發(fā)的模式、過程、技術和方法,其中包括UML模型圖到B方法形式規(guī)約的比較全面的轉換方法,實現形式規(guī)約的精化過程,形式化B方法的驗證技術,從UML形式化規(guī)約的逐步精化的規(guī)范與方法問題,整個規(guī)約、精化直到代碼生產階段的模型形式化驗證及自動化,基于B方法的面向對象軟件體系結構的形式化方法。通過該書的介紹使得學習者真正體會到如何應用形式化技術解決實際軟件開發(fā)技術問題。基于形式化方法的高可信軟件的開發(fā)基本走出實驗室,滿足高可信軟件開發(fā)的需要。