"1．內容全面，條理繫統。2．實例豐富，便於理解。3．理論充實，實踐性強4．文獻翔實，脈絡清晰。5．習題充足，利於掌握。6．附錄凝練，入門快速。"

●內容待完善

模型檢驗是一種對軟件和硬件繫統的可靠性進行自動驗證的形式化技術。使用這種技術，可以自動驗證和排除正在開發的繫統投入使用後是否存在影響繫統安全運行的微小瑕疵。本書全面、繫統、詳細地介紹了模型檢驗的邏輯和理論基礎、原理、驗證工具的使用方法以及軟件和硬件繫統的建模與驗證方法，主要內容包括繫統驗證、並發繫統的建模、線性時間性質、正則性質、線性時序邏輯、計算樹邏輯、等價和抽像、偏序約簡、時控自動機和概率繫統等10章。本書可作為計算機科學與技術、軟件工程、電子信息科學與技術及相關專業本科生、研究生的教材，也可作為模型檢驗領域研究人員及關注繫統可靠性的設計與開發人員的參考書。

(德)克裡斯特爾·拜耳,(德)喬斯特-皮爾特·卡托恩 著 趙光峰 等 譯