掃一掃
關注中圖網
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
用TLA+定義系統 TLA+語言與工具在軟硬件設計中的應用 版權信息
- ISBN：9787111678229
- 條形碼：9787111678229 ; 978-7-111-67822-9
- 裝幀：一般膠版紙
- 冊數：暫無
- 重量：暫無
- 所屬分類：>>
用TLA+定義系統 TLA+語言與工具在軟硬件設計中的應用 本書特色
適讀人群 ：測試人員、架構師、高級軟硬件開發設計人員、相關學術研究人員圖靈獎得主、TLA+開發者、微軟研究院首席研究員Leslie Lamport親筆撰寫，揭開并發和分布式計算的神秘面紗，系統架構形式化驗證**參考 隨著時代的發展，人們對各種信息系統的依賴越來越強，而這些系統也不再像傳統系統那樣封閉，它們面臨的挑戰和威脅與日俱增。為此，對于所謂的“非關鍵”信息系統而言，通過形式化技術提高設計質量、保證安全性與可靠性的需求也變得越來越迫切。 TLA+就是一種非常優秀的形式化建模語言。它的優點首先在于通用性，它可以描述大多數離散事件系統的行為邏輯；其次，它的難度適中，僅涉及CS專業大學本科階段的數學和計算機科學知識，能夠被廣大開發與設計人員所掌握；*后，由于TLA+的開發者（同時也是本書作者）的精心設計，它在驗證高并發、分布式等復雜邏輯方面具有獨特的優勢。 本書用形式化的建模和驗證方法保證所設計的軟硬件系統的正確性，結合若干案例，深入淺出地描述了從數學原理到系統建模的哲學思想，以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。
用TLA+定義系統 TLA+語言與工具在軟硬件設計中的應用 內容簡介
本書系統介紹了形式化建模語言TLA+以及模型檢查工具TLC，并結合若干案例，深入淺出地描述了從數學原理到系統建模的哲學思想，以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。本書分為五個部分。部分包含大多數程序員和工程師需要了解的有關編寫系統規約（即建立模型）的所有信息；第二部分包含更不錯的示例與材料，供需要進階的讀者使用；第三部分和第四部分為TLA+的參考手冊，包括語言本身的數學定義及工具的原理與使用；第五部分介紹在基礎TLA+上所演進出的TLA+版本2的新特性和少許變更。本書適合不錯軟硬件開發設計人員、測試人員、架構師以及相關學術研究人員閱讀。
用TLA+定義系統 TLA+語言與工具在軟硬件設計中的應用 目錄
出版者的話 譯者序 前言 致謝 **部分 入門 第1章 簡單數學基礎2 1.1 命題邏輯 2 1.2 集合4 1.3 謂詞邏輯 4 1.4 公式與陳述句 6 第2章 定義一個簡單時鐘 7 2.1 行為7 2.2 時鐘7 2.3 解讀規約 9 2.4 TLA+ 規約 10 2.5 規約的另一種寫法 12 第 3 章 異步接口示例 13 3.1 **個規約14 3.2 另一個規約17 3.3 類型回顧 18 3.4 定義 19 3.5 注釋 20 第 4 章 FIFO 接口示例23 4.1 內部規約 23 4.2 剖析實例化25 4.2.1 實例化是一種代換 25 4.2.2 參數化的實例化 26 4.2.3 隱式代換 26 4.2.4 不需重命名的實例化 27 4.3 隱藏內部變量 27 4.4 有界 FIFO 28 4.5 我們在定義什么 30 第 5 章 緩存示例31 5.1 內存接口 31 5.2 函數 33 5.3 可線性化內存系統 35 5.4 元組也是函數 37 5.5 遞歸函數定義 38 5.6 直寫式緩存39 5.7 不變式 44 5.8 證明實現 45 第 6 章 數學基礎拓展 47 6.1 集合 47 6.2 “笨表達式” 48 6.3 遞歸回顧 49 6.4 函數與運算符 51 6.5 函數使用 53 6.6 choose 54 第 7 章 編寫規約：一些建議 55 7.1 為什么要編寫規約 55 7.2 我們要定義什么 55 7.3 原子粒度 56 7.4 數據結構 57 7.5 編寫規約的步驟 57 7.6 進一步提示58 7.7 定義系統的時機和方法 60 第二部分 更多高級主題 第 8 章 活性和公平性 64 8.1 時態公式 64 8.2 時態重言式68 8.3 時態證明規則 71 8.4 弱公平性 71 8.5 內存規約 75 8.5.1 活性要求 75 8.5.2 換個表示法 76 8.5.3 推廣80 8.6 強公平性 81 8.7 直寫式緩存82 8.8 時態公式量化 84 8.9 時態邏輯剖析 85 8.9.1 回顧85 8.9.2 閉包85 8.9.3 閉包和可能性 87 8.9.4 轉化映射和公平性 87 8.9.5 活性不重要 89 8.9.6 時態邏輯讓人困惑 89 第 9 章 實時系統90 9.1 回顧時鐘規約 90 9.2 通用實時規約 93 9.3 實時緩存 96 9.4 Zeno 規約100 9.5 混合系統規約 102 9.6 關于實時103 第 10 章 組合規約 104 10.1 雙規約的組合 104 10.2 多規約的組合 107 10.3 FIFO 109 10.4 共享狀態的組合 111 10.4.1 顯式狀態變化 112 10.4.2 相交動作的組合 114 10.5 簡短回顧118 10.5.1 組合方法的分類 118 10.5.2 審視交錯規約 118 10.5.3 審視相交動作規約 118 10.6 活性和隱藏 119 10.6.1 活性和閉包119 10.6.2 隱藏 120 10.7 開放系統規約 121 10.8 接口轉化123 10.8.1 二進制時鐘123 10.8.2 轉化通道125 10.8.3 接口轉化推廣 128 10.8.4 開放系統規約 129 10.9 規約形式選擇 131 第 11 章 高級示例 132 11.1 定義數據結構 132 11.1.1 局部定義132 11.1.2 圖 134 11.1.3 求解微分方程 137 11.1.4 BNF 語法139 11.2 其他內存系統的規約 145 11.2.1 接口 146 11.2.2 正確性條件147 11.2.3 串行內存系統 148 11.2.4 順序一致內存系統 155 11.2.5 對內存規約的思考 161 第三部分 工具 第 12 章 語法分析器 164 第 13 章 TLATEX 排版器 166 13.1 引言 166 13.2 陰影效果的注釋 167 13.3 規約排版168 13.4 注釋排版168 13.5 調整輸出格式 170 13.6 輸出文件170 13.7 故障定位172 13.8 使用 LATEX 命令 172 第 14 章 TLC 模型檢查器 174 14.1 TLC 介紹174 14.2 TLC 的應用范圍 181 14.2.1 TLC 值181 14.2.2 TLC 如何計算表達式 182 14.2.3 賦值與代換184 14.2.4 計算時態公式 186 14.2.5 模塊覆蓋187 14.2.6 TLC 如何計算狀態 187 14.3 TLC 如何檢查屬性190 14.3.1 模型檢查模式 190 14.3.2 仿真模式192 14.3.3 視圖和指紋192 14.3.4 利用對稱性193 14.3.5 活性檢查的限制 195 14.4 TLC 模塊 196 14.5 TLC 的用法 198 14.5.1 運行 TLC 198 14.5.2 調試規約200 14.5.3 如何高效使用 TLC 204 14.6 TLC 不能做什么 207 14.7 附加說明208 14.7.1 配置文件語法 208 14.7.2 TLC 值的可比性 209 第四部分 TLA+ 語言 第 15 章 TLA+ 語法 218 15.1 簡化語法218 15.2 完整的語法 226 15.2.1 優先級與關聯性 226 15.2.2 對齊 229 15.2.3 注釋 230 15.2.4 時態公式231 15.2.5 兩種異常231 15.3 TLA+ 的詞素 232 第 16 章 TLA+ 的運算符 233 16.1 恒定運算符 233 16.1.1 布爾運算符234 16.1.2 選擇運算符236 16.1.3 布爾運算符的解釋 237 16.1.4 條件構造239 16.1.5 let/in 構造 240 16.1.6 集合運算符240 16.1.7 函數 242 16.1.8 記錄 245 16.1.9 元組 246 16.1.10 字符串 247 16.1.11 數字 248 16.2 非恒定運算符 249 16.2.1 基礎恒定表達式 249 16.2.2 狀態函數的含義 250 16.2.3 動作運算符251 16.2.4 時態運算符254 第 17 章 模塊的含義 257 17.1 運算符與表達式 257 17.1.1 運算符的元數與順序 257 17.1.2 ? 表達式 258 17.1.3 簡化運算符應用 259 17.1.4 表達式 260 17.2 級別 261 17.3 上下文 263 17.4 ? 表達式的含義 264 17.5 模塊的含義 265 17.5.1 引入 266 17.5.2 聲明 266 17.5.3 運算符定義267 17.5.4 函數定義267 17.5.5 實例化 267 17.5.6 定理與假設269 17.5.7 子模塊 269 17.6 模塊的正確性 270 17.7 尋找相關模塊 270 17.8 實例化的語義 271 第 18 章 標準模塊 276 18.1 Sequences 模塊276 18.2 FiniteSets 模塊 277 18.3 Bags 模塊277 18.4 關于數字的模塊 279 第五部分 TLA+ 版本 2 基礎 第 19 章 TLA+ 版本 2 286 19.1 簡介 286 19.2 遞歸運算符定義 286 19.3 lambda 表達式 288 19.4 定理與假設 288 19.4.1 命名 288 19.4.2 assume/prove 289 19.5 實例化 290 19.5.1 實例化詞綴運算符 290 19.5.2 Leibniz 運算符和實例化 291 19.6 命名子表達式 292 19.6.1 標簽和帶標簽的子表達式 名稱 292 19.6.2 位置相關的子表達式名稱 294 19.6.3 let 定義中的子表達式 297 19.6.4 assume/prove 的子表達式 297 19.6.5 將子表達式名稱用作運算符 298 19.7 證明的語法 298 19.7.1 證明的結構298 19.7.2 use、hide 與 by 300 19.7.3 當前狀態302 19.7.4 具有證明的步驟 303 19.7.5 無證明的步驟 306 19.7.6 對步驟與其組成部分的引用 308 19.7.7 對實例化的定理的引用 310 19.7.8 時態證明311 19.8 證明的語義 311 19.8.1 布爾運算符的含義 311 19.8.2 assume/prove 的含義 312 19.8.3 時態證明312
展開全部
用TLA+定義系統 TLA+語言與工具在軟硬件設計中的應用 作者簡介
萊斯利·蘭伯特（Leslie Lamport） 微軟研究院的首席研究員，2013年圖靈獎得主，美國國家科學院和國家工程院院士，LaTeX系統創始人。他是擁有杰出貢獻和輝煌成就的計算機大師、分布式系統領域的先鋒人物，他的分布式計算理論奠定了計算機學科的基礎。他于1978年發表的論文“Time, Clocks, and the Ordering of Events in a Distributed System”至今仍保持著計算機科學史上的被引用量紀錄。
書友推薦
- >
史學評論
- >
月亮與六便士
- >
羅庸西南聯大授課錄
- >
新文學天穹兩巨星--魯迅與胡適/紅燭學術叢書(紅燭學術叢書)
- >
我與地壇
- >
唐代進士錄
- >
隨園食單
- >
【精裝繪本】畫給孩子的中國神話
本類暢銷
