用TLA+定義系統(TLA+語言與工具在軟硬體設計中的應用)/中興通訊技術叢書/電腦科學叢書
內容大鋼
本書系統介紹了形式化建模語言TLA+以及模型檢查工具TLC，並結合若干案例，深入淺出地描述了從數學原理到系統建模的哲學思想，以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。本書分為五個部分。第一部分包含大多數程序員和工程師需要了解的有關編寫系統規約（即建立模型）的所有信息；第二部分包含更高級的示例與材料，供需要進階的讀者使用；第三部分和第四部分為TLA+的參考手冊，包括語言本身的數學定義及工具的原理與使用；第五部分介紹在基礎TLA+上所演進出的TLA+版本2的新特性和少許變更。
本書適合高級軟硬體開發設計人員、測試人員、架構師以及相關學術研究人員閱讀。
作者介紹
(美)萊斯利·蘭伯特|責編:王春華//孫榕舒|譯者:董路明//賀志平
萊斯利·蘭伯特（Lesie Lampot）微軟研究院的首席研究員，2013年圖靈獎得主，美國國家科學院和國家工程院院士，LaTeX系統刨始人。他是擁有傑出貢獻和輝煌成就的電腦大師、分散式系統領域的先鋒人物，他的分散式計算理論奠定了電腦學科的基礎。他于1978年發表的論文「Time, Clocks, and the Ordering of Events in a Distributed System」至今仍保持著電腦科學史上的被引用量紀錄。
目錄
出版者的話
譯者序
前言
致謝
第一部分 入門
第1章 簡單數學基礎
1.1 命題邏輯
1.2 集合
1.3 謂詞邏輯
1.4 公式與陳述句
第2章 定義一個簡單時鐘
2.1 行為
2.2 時鐘
2.3 解讀規約
2.4 TLA+規約
2.5 規約的另一種寫法
第3章 非同步介面示例
3.1 第一個規約
3.2 另一個規約
3.3 類型回顧
3.4 定義
3.5 註釋
第4章 FIFO介面示例
4.1 內部規約
4.2 剖析實例化
4.2.1 實例化是一種代換
4.2.2 參數化的實例化
4.2.3 隱式代換
4.2.4 不需重命名的實例化
4.3 隱藏內部變數
4.4 有界FIFO
4.5 我們在定義什麼
第5章 緩存示例
5.1 內存介面
5.2 函數
5.3 可線性化內存系統
5.4 元組也是函數
5.5 遞歸函數定義
5.6 直寫式緩存
5.7 不變式
5.8 證明實現
第6章 數學基礎拓展
6.1 集合
6.2 「笨表達式」
6.3 遞歸回顧
6.4 函數與運算符
6.5 函數使用
6.6 CHOOSE
第7章 編寫規約：一些建議
7.1 為什麼要編寫規約
7.2 我們要定義什麼
7.3 原子粒度
7.4 數據結構
7.5 編寫規約的步驟
7.6 進一步提示
7.7 定義系統的時機和方法
第二部分 更多高級主題
第8章 活性和公平性
8.1 時態公式
8.2 時態重言式
……
第三部分 工具
第四部分 TLA+語言
第五部分 TLA+版本2基礎
[