Handbook of Model Checking
暫譯: 模型檢查手冊

買這商品的人也買了...

相關主題

商品描述

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry.

 

The editors and authors of this handbook are among the world's leading researchers in this domain, and the 32 contributed chapters present a thorough view of the origin, theory, and application of model checking. In particular, the editors classify the advances in this domain and the chapters of the handbook in terms of two recurrent themes that have driven much of the research agenda: the algorithmic challenge, that is, designing model-checking algorithms that scale to real-life problems; and the modeling challenge, that is, extending the formalism beyond Kripke structures and temporal logic.

The book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools.

 

商品描述(中文翻譯)

模型檢查是一種電腦輔助的方法,用於分析可以通過狀態轉換系統建模的動態系統。模型檢查源自數學邏輯、程式語言、硬體設計和理論計算機科學的研究傳統,現在已廣泛應用於工業界的硬體和軟體驗證。

本手冊的編輯和作者是該領域的世界領先研究者,32篇貢獻章節全面介紹了模型檢查的起源、理論和應用。特別是,編輯們根據兩個反覆出現的主題對該領域的進展和手冊的章節進行分類:算法挑戰,即設計能夠擴展到現實問題的模型檢查算法;以及建模挑戰,即將形式化擴展到超越 Kripke 結構和時間邏輯的範疇。

本書對於從事形式方法和驗證工具開發的研究人員和研究生將具有重要價值。