当前位置:网站首页>TLA+ 入门教程(1):形式化方法简介
TLA+ 入门教程(1):形式化方法简介
2022-07-04 21:39:00 【InfoQ】
- 1、采用工程方法来组织、管理软件的开发过程;
- 2、深入探讨程序和程序开发过程的规律,建立严密的理论,推演和验证理论的正确性,用来指导软件开发实践。
什么是 TLA+
- 系统所有的变量
- 这些变量的初始值是什么
- 哪些动作让变量的状态发生改变,这些变量在当前状态下的值与它们在下一个状态下的可能值之间的关系
写在后面,TLA+ 真的有用吗?
- Intel 将 TLA+ 用于工业硬件建模,帮助工程师在实际构建之前进行思考;
- AWS 从 2011 年开始使用 TLA+,TLA+ 模型检查在 DynamoDB,S3,EBS 和内部分布式锁管理器中均检测出了难以发现的潜在错误,AWS 已经发表了数篇形式化方法的论文;
- Microsoft 在 Xbox 360,Azure 中都有使用 TLA+,还使用 TLA+ 设计了 Cosmos DB[8];
- 一款以网络为中心的 RTOS 应用案例;
- 对各种分布式共识算法(Paxos、Raft 和 EPaxos 等)都提供其 TLA+ 验证;
参考引用
边栏推荐
- 1807. Replace the parentheses in the string
- [leetcode] 17. Letter combination of telephone number
- Bookmark
- Spatiotemporal prediction 3-graph transformer
- Interpreting the development of various intelligent organizations in maker Education
- GTEST from ignorance to proficiency (4) how to write unit tests with GTEST
- Go language loop statement (3 in Lesson 10)
- 广电五舟与华为签署合作协议,共同推进昇腾AI产业持续发展
- Interviewer: what is XSS attack?
- Enlightenment of maker thinking in Higher Education
猜你喜欢
KDD2022 | 什么特征进行交互才是有效的?
Deveco device tool 3.0 release brings five capability upgrades to make intelligent device development more efficient
应用实践 | 蜀海供应链基于 Apache Doris 的数据中台建设
HUAWEI nova 10系列发布 华为应用市场筑牢应用安全防火墙
el-tree结合el-table,树形添加修改操作
TCP shakes hands three times and waves four times. Do you really understand?
From repvgg to mobileone, including mobileone code
Interpreting the development of various intelligent organizations in maker Education
并发优化总结
gtest从一无所知到熟练使用(3)什么是test suite和test case
随机推荐
Interview question 01.01 Determine whether the character is unique
HDU - 1078 fatmouse and cheese (memory search DP)
GTEST from ignorance to proficiency (4) how to write unit tests with GTEST
解决异步接口慢导致的数据错乱问题
[weekly translation go] how to code in go series articles are online!!
超详细教程,一文入门Istio架构原理及实战应用
MongoDB中的索引操作总结
283. Moving zero-c and language assisted array method
面试题 01.08. 零矩阵
HDU - 1078 FatMouse and Cheese(记忆化搜索DP)
Deveco device tool 3.0 release brings five capability upgrades to make intelligent device development more efficient
Visual task scheduling & drag and drop | scalph data integration based on Apache seatunnel
Acwing 2022 daily question
TCP shakes hands three times and waves four times. Do you really understand?
做BI开发,为什么一定要熟悉行业和企业业务?
删库不必跑路!详解 MySQL 数据恢复
How is the entered query SQL statement executed?
能源势动:电力行业的碳中和该如何实现?
Redis has three methods for checking big keys, which are necessary for optimization
NAACL-22 | 在基于Prompt的文本生成任务上引入迁移学习的设置