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