Model Checking, 2/e (Hardcover)

Edmund M. Clarke Jr., Orna Grumberg, Daniel Kroening, Doron Peled, Helmut Veith

  • 出版商: MIT
  • 出版日期: 2018-12-04
  • 售價: $1,560
  • 貴賓價: 9.8$1,529
  • 語言: 英文
  • 頁數: 424
  • 裝訂: Hardcover
  • ISBN: 0262038838
  • ISBN-13: 9780262038836
  • 立即出貨 (庫存=1)

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

商品描述

An expanded and updated edition of a comprehensive presentation of the theory and practice of model checking, a technology that automates the analysis of complex systems.

Model checking is a verification technology that provides an algorithmic means of determining whether an abstract model―representing, for example, a hardware or software design―satisfies a formal specification expressed as a temporal logic formula. If the specification is not satisfied, the method identifies a counterexample execution that shows the source of the problem. Today, many major hardware and software companies use model checking in practice, for verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. This book offers a comprehensive presentation of the theory and practice of model checking, covering the foundations of the key algorithms in depth.

The field of model checking has grown dramatically since the publication of the first edition in 1999, and this second edition reflects the advances in the field. Reorganized, expanded, and updated, the new edition retains the focus on the foundations of temporal logic model while offering new chapters that cover topics that did not exist in 1999: propositional satisfiability, SAT-based model checking, counterexample-guided abstraction refinement, and software model checking. The book serves as an introduction to the field suitable for classroom use and as an essential guide for researchers.

商品描述(中文翻譯)

這是一本關於模型檢查理論和實踐的擴充和更新版。模型檢查是一種驗證技術,提供了一種算法手段,用於確定抽象模型(例如硬件或軟件設計)是否滿足以時間邏輯公式表示的形式化規範。如果規範不滿足,該方法將識別出一個反例執行,顯示問題的來源。如今,許多主要的硬件和軟件公司在實踐中使用模型檢查,用於驗證VLSI電路、通信協議、軟件設備驅動程序、實時嵌入式系統和安全算法。本書全面介紹了模型檢查的理論和實踐,深入探討了關鍵算法的基礎。

自1999年第一版出版以來,模型檢查領域已經有了巨大的發展,這本第二版反映了該領域的進步。新版重新組織、擴充和更新,保持了對時間邏輯模型基礎的關注,同時增加了1999年不存在的主題章節:命題可滿足性、基於SAT的模型檢查、反例引導的抽象修正和軟件模型檢查。本書既適合作為課堂教學的入門指南,也是研究人員的必備指南。