| ISBN/价格： | 978-7-111-67822-9:CNY139.00 |
|---|
| 作品语种： | chi eng |
|---|
| 出版国别： | CN 110000 |
|---|
| 题名责任者项： | 用TLA+定义系统/.(美)莱斯利·兰伯特(Leslie Lamport)著/.董路明，贺志平译 |
|---|
| 出版发行项： | 北京:,机械工业出版社:,2021.04 |
|---|
| 载体形态项： | 13,314页:;+图:;+26cm |
|---|
| 丛编项： | 中兴通讯技术丛书 |
|---|
| 丛编项： | 计算机科学丛书 |
|---|
| 提要文摘： | 本书是作者针对分布式并发计算系统超过25年的研究成果的总结。在本书中，作者提出用基于动作的时态逻辑(TLA)来为复杂信息系统的行为建立数学模型，进而使用严格的数学证明与检验的方法来验证系统行为的正确性。为此，作者发明了建模语言TLA+以及模型检查工具TLC。本书结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。 |
|---|
| 并列题名： | Specifying systems eng |
|---|
| 题名主题： | 并发程序设计 |
|---|
| 中图分类： | TP311.11 |
|---|
| 个人名称等同： | 兰伯特 莱斯利 (美) 著 |
|---|
| 个人名称次要： | 董路明 译 |
|---|
| 个人名称次要： | 贺志平 译 |
|---|
| 记录来源： | CN 人天书店 20210512 |
|---|