Principles of Model Checking (Hardcover)

Christel Baier, Joost-Pieter Katoen

  • 出版商: MIT
  • 出版日期: 2008-05-01
  • 售價: $2,800
  • 貴賓價: 9.8$2,744
  • 語言: 英文
  • 頁數: 984
  • 裝訂: Hardcover
  • ISBN: 026202649X
  • ISBN-13: 9780262026499
  • 相關翻譯: 模型檢驗原理 (簡中版)
  • 立即出貨 (庫存=1)

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

商品描述

Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, or request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field.

The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.

商品描述(中文翻譯)

我們對越來越複雜的電腦和軟體系統的依賴日益增長,這就需要開發形式化、技術和工具來評估這些系統的功能特性。在過去二十年中出現了一種名為模型檢查的技術,它系統地(並自動地)檢查一個給定系統的模型是否滿足死結自由、不變量或請求-回應特性等所需的屬性。這種自動化的驗證和調試技術已經發展成為一種成熟且廣泛應用的方法,具有許多應用領域。《模型檢查原理》提供了一個全面介紹模型檢查的教材,不僅適合課堂使用,也是該領域研究人員和從業人員的寶貴參考資料。

本書首先介紹了建模並發和通信系統的基本原則,介紹了不同類型的屬性(包括安全性和活性),介紹了公平性的概念,並提供了基於自動機的算法來檢驗這些屬性。它介紹了時態邏輯LTL和CTL,並對它們進行比較,並涵蓋了驗證這些邏輯的算法,討論了實時系統以及受隨機現象影響的系統。單獨的章節介紹了提高效率的技術,如抽象和符號操作。本書包含了大量的例子(其中大部分貫穿了幾個章節),以及一套完整的基本結果和詳細的證明。每章結束時都有一個摘要、參考文獻和大量的實際和理論性質的練習題。