6月25日·直播丨软件开发中,如何发现并发系统中的隐藏错误?

51fusa安全社区联合旗下 原创技术内容品牌「鉴源实验室」，推出鉴源精选文章系列分享课程，邀请主笔文章的行业权威专家、资深从业者，围绕当前工控领域高热点、最前沿的技术内容进行深入解读。

6月25日（本周四）20:00，课程将特邀上海控安可信软件创新研究院，系统建模组研发工程师，肖圣平博士，分享“软件开发中，如何发现并发系统中的隐藏错误？”主题课程。欢迎各位感兴趣的小伙伴扫描下方海报二维码，入群与老师交流学习~

关注公众号“鉴源实验室”

了解更多前沿技术

直播安排 Schedule

时间：6月25日（本周四）20:00

地点：线上学堂

流程：

主题介绍

课程主题 Theme

软件开发中，如何发现并发系统中的隐藏错误？

分享内容 Contents

随着社会和技术的高速发展，“变”与“不确定性”越来越成为主旋律，乌卡时代已经来临。为了快速响应外界的变化，相比于传统的工作方式，敏捷(Agile)可以很好的响应变化，已经成为了数字化时代的标配，被越来越多的行业和企业所采用。

在软件开发中，有些问题很容易通过测试暴露出来：给定一个输入，程序输出不符合预期；调用一个接口，返回结果明显错误；执行一个功能，系统直接崩溃。这类问题虽然也可能定位困难，但至少通常有比较明确的触发条件。并发系统中的很多错误不是这样。它们并不稳定出现，也不一定由某个特殊输入直接触发。更常见的情况是，大多数时候系统运行正常，只有在某个特定的线程调度顺序、消息到达顺序、超时触发时机或重试路径下，系统才会进入错误状态。

普通测试当然很重要，但测试通常只能覆盖有限的输入、有限的场景和有限的调度顺序。一个并发程序跑了一千次没有问题，并不代表所有可能的线程交错、消息顺序和状态变化都没有问题。于是，一个自然的问题出现了：有没有一种方法，可以不只是跑几个测试样例，而是更系统地检查系统中可能发生的行为路径？围绕这个问题，研究人员发展出了模型检查（Model Checking）这一类形式化验证方法。本期介绍的Spin，正是模型检查领域最经典、最有代表性的工具之一。理解Spin，不只是认识一个工具，更是理解一种思维方式：不要只问“我测试过的场景有没有问题”，还要问“系统所有可能发生的行为中，是否存在一条路径会走向错误”。

精讲要点：

1. Spin是什么

2. 为什么需要Spin

3. Spin检查的是抽象后的系统行为

4. Spin的基本工作方式

5. 理解Spin需要掌握的几个关键词

……

讲师介绍 Lecturer

肖圣平博士，毕业于华东师范大学软件工程学院，目前担任上海控安可信软件创新研究院系统建模组研发工程师，主要负责程序验证与形式化方法的相关研发工作。