本書是作者針對分布式並發計算繫統超過25年的研究成果的總結。在本書中,作者提出用基於動作的時態邏輯(TLA)來為復雜信息繫統的行為建立數學模型,進而使用嚴格的數學證明與檢驗的方法來驗證繫統行為的正確性。為此,作者發明了建模語言TLA 以及模型檢查工具TLC。本書結合若干案例,深入淺出地描述了從數學原理到繫統建模的哲學思想,以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。
本書分為五個部分。部分包含大多數程序員和工程師需要了解的有關編寫繫統規約(即建立模型)的所有信息;第二部分包含更高級的示例與材料,供需要進階的讀者使用;第三部分和第四部分為TLA 的參考手冊,包括語言本身的定義及工具的原理與使用;第五部分介紹在基礎TLA 語言上所演進出的TLA 版本2的新特性和少許變更。