作　　者： 古天龍　編 出 版 社： 高等教育出版社 形式化方法是建立在嚴格數學基礎上、具有精確數學語義的開發方法。從廣義角度，形式化方法是軟件開發過程中分析、設計及實現的系統工程方法。狹義地，形式化方法是軟件規格和驗證的方法。本書對軟件開發中的形式化方法進行了介紹和討論，內容涵蓋了SE2004中關于“軟件的形式化方法”的知識點，主要包括：有限狀態機、Statecharts、Petri網、通信順序進程、通信系統演算、一階邏輯、程序正確性證明、時態邏輯、模型檢驗、Z、VDM、 Larch等。 　　本書可作為計算機、軟件工程等專業高年級本科聲或研究生的教學用書，也可供相關領域的研究人員和工程技術人員參考。