注册 / 登录

正确性驱动建模:用TLA+进行系统设计

分会场:  架构演进/工程实践/大前端

分享时间: 2017年11月9日 - 12日

案例来源 :

案例讲师

孙鸣

中兴通讯 资深系统架构师

孙鸣,中兴通讯资深系统架构师,17年软件系统设计、架构经验。国内敏捷方法最早的践行者。敏捷领域两本重要著作《平衡敏捷与规范》以及《敏捷软件开发:原则、模式与实践(C#)》的中文译者,《Erlang趣学指南》的中文译者。从2001年起,在IBM DeveloperWorks等开发者媒体上发表关于敏捷、软件设计、测试等技术文章十数篇。2007年带领团队自主研发设高性能海量数据存储引擎,成功替换产品中商用数据库。2010年在公司内开创软件设计类培训,开发原创性培训课件数十件,迄今为止历时8年,受训学员达数千人。2011年,在中国敏捷软件开发者大会上做了“敏捷架构风格”的演讲。

扫描二维码分享案例

 

案例简述

 

通常,我们在进行系统设计时都是基于一些先验知识和假设的。我们熟悉架构设计的模式,掌握领域驱动设计的方法,了解常用的基础设施组件等,基于此给出一个合格的架构设计不是一件非常困难的事情。不过,如果想在设计上有所创新、有所突破,让设计更加清晰、简单、可靠,特别是想凸显出设计的正确性,就不是那么容易了。系统越庞大、复杂就越是如此,看看我们在设计评审、代码走查、测试上的投入和最终产品质量的表现之间是多么的不平衡就充分说明了这一点。



究其原因,是因为以上述方式设计时,存在3个方面比较严重的问题:

1、 设计中最基本的是要先清晰、精确、严格地描述出所期望的系统行为,而我们在设计时要么忽视了这一点,要么对系统行为的描述非常含糊、不准确。

2、 在设计中,虽然我们也强调抽象,但大多是实现层面的抽象,而非系统行为层面的抽象。这样做在设计时就引入了不必要的复杂性,并且会遗漏掉很多合理的系统行为。

3、 在设计时,对于正确性基本没有规范的考虑,无法给出规范的设计正确性属性,这样做会导致设计看起来很漂亮,但是隐藏着不少不那么明显的错误。



TLA+是图灵奖得主Leslie Lamport发明的专门用来描述并验证复杂系统行为的形式化方法。和其他同类方法不同,TLA+从一开始就考虑到实效性,它的目标用户就是一线的开发工程师和架构师,学习TLA+仅需要初级的数学基础(简单的集合论和一阶逻辑知识,复杂时态逻辑部分完全被隐藏在下面)。TLA+可以迫使我们回到问题的根本,从新思考那些先验知识和假设,在一个更高的抽象层次上精确地描述系统的行为和正确性属性,并进行自动化的正确性验证,从而得到一个更加简单、清晰、正确的架构。Aamazon、Microsoft、Intel以及Oracle等业界领先软件企业的核心产品都在使用TLA+,并获益良多。



在本案例中,我将给大家介绍TLA+的原理、思维方式以及它的工具链,并会以一个分布式集群不间断服务升级部署系统的设计为例,介绍如何使用TLA+,以正确性为驱动进行系统建模和设计。

 

案例目标

 

通常,我们在进行系统设计时都是基于一些先验知识和假设的。我们熟悉架构设计的模式,掌握领域驱动设计的方法,了解常用的基础设施组件等,基于此给出一个合格的架构设计不是一件非常困难的事情。不过,如果想在设计上有所创新、有所突破,让设计更加清晰、简单、可靠,特别是想凸显出设计的正确性,就不是那么容易了。系统越庞大、复杂就越是如此,看看我们在设计评审、代码走查、测试上的投入和最终产品质量的表现之间是多么的不平衡就充分说明了这一点。
究其原因,是因为以上述方式设计时,存在3个方面比较严重的问题: 1、 设计中最基本的是要先清晰、精确、严格地描述出所期望的系统行为,而我们在设计时要么忽视了这一点,要么对系统行为的描述非常含糊、不准确。 2、 在设计中,虽然我们也强调抽象,但大多是实现层面的抽象,而非系统行为层面的抽象。这样做在设计时就引入了不必要的复杂性,并且会遗漏掉很多合理的系统行为。 3、 在设计时,对于正确性基本没有规范的考虑,无法给出规范的设计正确性属性,这样做会导致设计看起来很漂亮,但是隐藏着不少不那么明显的错误。

 

成功(或教训)要点

 

1、 设计中最基本的是要先清晰、精确、严格地描述出所期望的系统行为
2、 设计时要重点考虑系统行为层面的抽象,不要因为实现的限制而遗漏掉合理的系统行为。
3、 TLA+是图灵奖得主Leslie Lamport发明的专门用来描述并验证复杂系统行为的形式化方法,使用TLA+可以帮助我们在设计时,基于系统层面的抽象对系统的正确性做形式化、规范的描述,并且定义出设计的正确性属性,自动化地加以验证,以正确性为驱动进行系统建模和设计。

 

案例ROI分析

 

和其他同类系统行为形式化方法不同,TLA+从一开始就考虑到实效性,它的目标用户就是一线的开发工程师和架构师,学习TLA+仅需要初级的数学基础(简单的集合论和一阶逻辑知识,复杂时态逻辑部分完全被隐藏在下面)。所以很容易为一线的开发工程师和架构师掌握和运用。它既适用于高层的系统设计,也适用于低层代码层面的逻辑验证。能够准确给出设计中的核心关键属性和逻辑,定义出系统的行为集合,并在设计早期就对设计的正确性加以验证,有了TLA+ SPEC,可以极大地降低研发中的沟通成本和后期测试成本,并能有效降低设计的复杂性、为实现中创新提供保障。

 

案例启示

 

TLA+可以迫使我们回到问题的根本,从新思考那些先验知识和假设,在一个更高的抽象层次上精确地描述系统的行为和正确性属性,并进行自动化的正确性验证,从而得到一个更加简单、清晰、正确的架构。