本書從軟件實際開發過程出發，將形式化技術應用于每個開發階段，系統地介紹了基于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章 過程模型在平臺上實現的關鍵技術
主要參考文獻
索引
新書資訊