内容简介:
随着互联网、电信、云计算等超大型系统的越来越广泛应用,这种系统特征都是业务状态和状态组合及其丰富,动态特性交错耦合严重,并伴随高并发、高可用性的系统约束,这种情况下,级联故障、转弯故障、业务状态不一致、条件竞争故障等问题会层出不穷,其根因是设计构造的缺失,并且很难复现、定位和解决。这些问题给系统带来的不是好不好用,而是能不能用的问题。
TLA+可以提供一种轻量级建模和验证系统约束的手段,对系统进行离散化和符号化,然后使用数学语言进行形式化的描述并建立动态模型,接着对模型中状态组合进行穷举,把违反系统约束的状态和产生该状态的路径进行显式的标识,从而识别缺失的设计构造,达到较高的设计验证投入比,非常值得推荐。
演讲题纲:
1.系统本质复杂度越来越高;
2.其他工程技术领域如何建模应对复杂度的提升; 3.软件领域如何应对复杂度提升; 4.通过案例演示tla+建模和验证系统完备性。听众收益:
1.了解软件复杂度的变化的规律;
2.了解什么是形式化建模?
3.了解tla+的应用场景和使用步骤。