用TLA+定义系统 TLA+语言与工具在软硬件设计中的应用
- ISBN:9787111678229
- 装帧:一般胶版纸
- 册数:暂无
- 重量:暂无
- 开本:16开
- 页数:328
- 出版时间:2021-04-01
- 条形码:9787111678229 ; 978-7-111-67822-9
本书特色
适读人群 :测试人员、架构师、高级软硬件开发设计人员、相关学术研究人员图灵奖得主、TLA+开发者、微软研究院首席研究员Leslie Lamport亲笔撰写,揭开并发和分布式计算的神秘面纱,系统架构形式化验证**参考 随着时代的发展,人们对各种信息系统的依赖越来越强,而这些系统也不再像传统系统那样封闭,它们面临的挑战和威胁与日俱增。为此,对于所谓的“非关键”信息系统而言,通过形式化技术提高设计质量、保证安全性与可靠性的需求也变得越来越迫切。 TLA+就是一种非常优秀的形式化建模语言。它的优点首先在于通用性,它可以描述大多数离散事件系统的行为逻辑;其次,它的难度适中,仅涉及CS专业大学本科阶段的数学和计算机科学知识,能够被广大开发与设计人员所掌握;*后,由于TLA+的开发者(同时也是本书作者)的精心设计,它在验证高并发、分布式等复杂逻辑方面具有独特的优势。 本书用形式化的建模和验证方法保证所设计的软硬件系统的正确性,结合若干案例,深入浅出地描述了从数学原理到系统建模的哲学思想,以及从建模语言的工程实践到模型验证工具的运用技巧等内容。
内容简介
本书系统介绍了形式化建模语言TLA+以及模型检查工具TLC,并结合若干案例,深入浅出地描述了从数学原理到系统建模的哲学思想,以及从建模语言的工程实践到模型验证工具的运用技巧等内容。本书分为五个部分。部分包含大多数程序员和工程师需要了解的有关编写系统规约(即建立模型)的所有信息;第二部分包含更不错的示例与材料,供需要进阶的读者使用;第三部分和第四部分为TLA+的参考手册,包括语言本身的数学定义及工具的原理与使用;第五部分介绍在基础TLA+上所演进出的TLA+版本2的新特性和少许变更。本书适合不错软硬件开发设计人员、测试人员、架构师以及相关学术研究人员阅读。
目录
作者简介
莱斯利·兰伯特(Leslie Lamport) 微软研究院的首席研究员,2013年图灵奖得主,美国国家科学院和国家工程院院士,LaTeX系统创始人。他是拥有杰出贡献和辉煌成就的计算机大师、分布式系统领域的先锋人物,他的分布式计算理论奠定了计算机学科的基础。他于1978年发表的论文“Time, Clocks, and the Ordering of Events in a Distributed System”至今仍保持着计算机科学史上的被引用量纪录。
-
Photoshop图像处理标准培训教程
¥20.4¥68.0 -
写给小白的Python入门实战课
¥16.0¥50.0 -
翻转世界-互联网思维与新技术如何改变未来
¥16.0¥49.9 -
Excel 实战应用大全
¥15.9¥49.8 -
物联网关键技术及其数据处理研究
¥19.1¥59.8 -
人工智能技术丛书神经网络与深度学习
¥111.8¥149.0 -
多功能智能机器小车的开发与研制
¥17.9¥56.0 -
由浅入深学习SAP财务
¥67.3¥118.0 -
APP INVENTOR少儿趣味编程动手做
¥18.9¥59.0 -
机器学习导论
¥47.4¥79.0 -
网络社团结构成因探究及其对网络中同步动力学行为的影响
¥32.9¥45.0 -
网络节点异质性预测研究及其对网络中信息-疾病耦合动力学行为的影响
¥32.9¥45.0 -
智能优化算法及MATLAB实现
¥83.8¥99.8 -
PYTORCH深度学习指南:编程基础 卷I
¥74.3¥99.0 -
智能图像处理技术及应用研究
¥35.8¥65.0 -
MATLAB计算机视觉与深度学习实战(第2版)
¥101.1¥128.0 -
人工智能+机器人入门与实战(修订版)用树莓派+Python+OpenCV制作计算
¥53.0¥69.8 -
系统集成项目管理工程师考试大纲(
¥12.9¥15.0 -
PYTHON GUI设计TKINTER 菜鸟编程(增强版)
¥70.3¥99.0 -
企业级应用开发实战
¥41.9¥59.9