形式化方法是指有嚴格數學基礎的軟件和系統開發(fā)方法,支持軟件與系統的規(guī)約、設計、驗證與演化等活動。隨著軟件可信需求的不斷增長,形式化方法的重要性和關注度日益提高。全書共12章,第1章概述形式化方法,第2章介紹形式化方法發(fā)展早期的經典內容,其余部分共分3篇: 上篇(第3~5章)為系統建模篇,著重介紹遷移系統、有窮自動機、Petri網等基本計算模型; 中篇(第6和第7章)為形式規(guī)約篇,著重討論時序邏輯及其在并發(fā)系統屬性描述的應用; 下篇(第8~12章)為形式驗證篇,除介紹演繹證明方法外,著重介紹驗證并發(fā)、實時及混成系統的各種模型檢測方法及相關驗證工具。全書提供了大量應用實例,每章后均附有習題。本書適合作為高等院校計算機、軟件工程、網絡工程、信息安全、自動化等專業(yè)高年級本科生、研究生的教材,同時可供相關領域的研究人員和技術開發(fā)人員參考。