K+全球软件研发行业创新峰会

内容简介：
随着互联网、电信、云计算等超大型系统的越来越广泛应用，这种系统特征都是业务状态和状态组合及其丰富，动态特性交错耦合严重，并伴随高并发、高可用性的系统约束，这种情况下，级联故障、转弯故障、业务状态不一致、条件竞争故障等问题会层出不穷，其根因是设计构造的缺失，并且很难复现、定位和解决。这些问题给系统带来的不是好不好用，而是能不能用的问题。 TLA+可以提供一种轻量级建模和验证系统约束的手段，对系统进行离散化和符号化，然后使用数学语言进行形式化的描述并建立动态模型，接着对模型中状态组合进行穷举，把违反系统约束的状态和产生该状态的路径进行显式的标识，从而识别缺失的设计构造，达到较高的设计验证投入比，非常值得推荐。

演讲题纲：

1.系统本质复杂度越来越高；

听众收益：

1.了解软件复杂度的变化的规律； 2.了解什么是形式化建模？ 3.了解tla+的应用场景和使用步骤。