潍坊科技学院图书馆书目检索系统

Online Public Access Catalogue

题名/责任者:

用TLA+定义系统/(美)莱斯利·兰伯特(Leslie Lamport)著

出版发行项:

北京:机械工业出版社,2021

ISBN及定价:

978-7-111-67822-9/CNY139.00

载体形态项:

328页;26cm

个人责任者:

著 兰伯特

个人次要责任者:

董路明

中图法分类号:

TP311.11

提要文摘附注:

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

使用对象附注:

并发程序设计相关人员

豆瓣简介：