幫助中心 | 我的帳號 | 關於我們
進階搜尋
car

同類熱銷排行榜

最近瀏覽的商品

模型檢測

  • 作者：(美)Edmund M.Clarke//Orna Grumberg//Doron A.Peled|譯者:吳盡昭//何安平//高新岩
  • 出版社：電子工業
  • ISBN：9787121352744
  • 出版日期：2018/11/01
  • 裝幀：平裝
  • 頁數：225
人民幣：RMB 69 元      售價：元
放入購物車
加入收藏夾
內容大鋼
    模型檢測是一種用於自動驗證有限狀態併發系統的技術，與基於模擬、測試和演繹推理的傳統技術相比，具有許多方面的優勢。Edmund M.Clarke，Orna Grumberg，Doron A.Peled著的《模型檢測》共分18章，涵蓋的主要內容包括模型檢測的基本知識、系統建模、時序邏輯、符號模型檢測技術、SMV模型檢測器、模型檢測與自動機理論、偏序約簡、抽象解釋、有限狀態系統的無限簇、實時系統驗證等。
    本書既適合從事電腦科學、電子科學、電氣工程、工業製造等複雜系統研究的科研人員閱讀，也適合系統管理、測試部門的企事業單位人員作為參考用書。
作者介紹
(美)Edmund M.Clarke//Orna Grumberg//Doron A.Peled|譯者:吳盡昭//何安平//高新岩
    Edmund M.Clarke教授，美國卡內基·梅隆大學電腦科學系教授，並且是ACM和IEEE會士。他在軟硬體驗證、自動定理證明、形式方法等方面享有崇高的國際聲譽，2007年獲得ACM圖靈獎。
目錄
第1章  緒論
  1.1  形式化方法的需求
  1.2  硬體與軟體驗證
  1.3  模型檢測的流程
  1.4  時序邏輯與模型檢測
  1.5  符號演算法
  1.6  偏序約簡
  1.7  緩解狀態爆炸問題的其他方法
第2章  系統建模
  2.1  併發系統建模
  2.2  併發系統
  2.3  程序翻譯的實例
第3章  時序邏輯
  3.1  計算樹邏輯CTL
  3.2  CTL和LTL邏輯
  3.3  公正性
第4章  模型檢測
  4.1  CTL模型檢測
  4.2  基於tableau結構的LTL模型檢測
  4.3  CTL模型檢測
第5章  二叉判定圖
  5.1  布爾公式的表示方法
  5.2  Kripke結構的表示方法
第6章  符號模型檢測
  6.1  不動點表示
  6.2  CTL符號模型檢測
  6.3  符號模型檢測中的公正性
  6.4  反例和診斷信息
  6.5  一個ALU的例子
  6.6  關係積的計算
  6.7  符號化的LTL模型檢測
第7章  基於μ演算的模型檢測
  7.1  簡介
  7.2  命題μ演算
  7.3  求不動點公式的值
  7.4  用OBDD表示μ演算公式
  7.5  將CTL公式轉化為μ演算
  7.6  複雜度問題
第8章  實踐中的模型檢測
  8.1  SMV模型檢測器
  8.2  一個實際的例子
第9章  模型檢測和自動機理論
  9.1  有限字與無限字上的自動機
  9.2  使用自動機進行模型檢測
  9.3  檢查B?chi自動機接受的語言是否為空
  9.4  LTL公式轉化為自動機
  9.5  採用「On-the-Fly」技術的模型檢測
  9.6  檢測語言包含的符號方法
第10章  偏序約簡
  10.1  非同步系統中的併發

  10.2  獨立性與不可見性
  10.3  LTL-X的偏序約簡
  10.4  一個例子
  10.5  計算充足集(ample)集合
  10.6  演算法的正確性
  10.7  SPIN系統中的偏序約簡
第11章  結構間的等價性和擬序
  11.1  等價和擬序演算法
  11.2  構建tableau結構
第12章  組合推理
  12.1  多個結構的組合
  12.2  判斷假設保證證明方法的正確性
  12.3  CPU控制器的驗證
第13章  抽象
  13.1  影響錐化簡
  13.2  數值抽象
第14章  對稱性
  14.1  群和對稱性
  14.2  商模型
  14.3  對稱性和模型檢測
  14.4  複雜度問題
  14.5  實驗結果
第15章  有限狀態系統的無限簇
  15.1  無限簇上的時序邏輯
  15.2  不變數
  15.3  再次分析Futurebus+
  15.4  圖和網路文法
  15.5  令牌環簇的不確定性結果
第16章  離散實時系統和定量時序分析
  16.1  實時系統和單調變化率調度
  16.2  實時系統的模型檢測
  16.3  RTCTL模型檢測
  16.4  量化時序的分析：最小或最大延遲
  16.5  飛行控制器
第17章  連續實時系統
  17.1  時間約束自動機
  17.2  並行組合
  17.3  使用時間約束自動機進行建模
  17.4  時鐘域
  17.5  時鐘區
  17.6  邊界可區分矩陣
  17.7  複雜度問題
第18章  結論
參考文獻

  • 商品搜索：
  • | 高級搜索
首頁│ 新手上路│ 客服中心│ 關於我們│ 聯絡我們│ Top↑│
Copyrightc 1999~2008 美商天龍國際圖書股份有限公司 臺灣分公司. All rights reserved.
營業地址:臺北市中正區重慶南路一段103號1F 105號1F-2F
讀者服務部電話：02-2381-2033 02-2381-1863　時間：週一-週五 10:00-17:00
　服務信箱：bookuu@69book.com 客戶、意見信箱:cs@69book.com
ICP證：浙B2-20060032