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