机读格式显示(MARC)

• 000 00948nam0 2200217 450

• 001 0000514715

• 010 __ |a 978-7-111-67822-9 |d CNY139.00

• 092 __ |b 百万庄15502300314

• 100 __ |a 20210421d2021 em y0chiy50 ea

• 102 __ |a CN |b 110000

• 200 __ |a 用TLA+定义系统 |f (美)莱斯利·兰伯特(Leslie Lamport)著

• 210 __ |a 北京 |c 机械工业出版社 |d 2021

• 215 __ |a 328页 |d 26cm

• 330 __ |a 本书是作者针对分布式并发计算系统超过25年的研究成果的总结。在本书中，作者提出用基于动作的时态逻辑（TLA）来为复杂信息系统的行为建立数学模型，进而使用严格的数学证明与检验的方法来验证系统行为的正确性。为此，作者发明了建模语言TLA+以及模型检查工具TLC。本书结合若干案例，深入浅出地描述了从数学原理到系统建模的哲学思想，以及从建模语言的工程实践到模型验证工具的运用技巧等内容。

• 333 __ |a 并发程序设计相关人员

• 690 __ |a TP311.11 |v 5

• 701 __ |4 著 |a 兰伯特

• 702 __ |a 董路明

• 801 _0 |a CN |b WFKJXY |c 20210927

• 905 __ |a WFKJXY |d TP311.11/26

• 920 __ |a 4370400 |z 1