2020年第十一届中国国际软件质量工程（iSQE）峰会特邀华东师范大学副教授陈小红副教授分享“安全需求的一致性验证方法研究”。安全需求的一致性验证是安全攸关系统一项重要但仍然具有挑战性的任务。这主要是因为安全要求通常是用自然语言编写的，并且具有很强的时间限制，但它需要形式化的精确验证。从工业对铁路联锁系统的实际需求出发，提出用伪自然语言（模式语言）描述安全需求，对其进行形式化，并提供系列方法自动安全需求的一致性。在演讲中我将介绍三种验证方法，基于Z3的有界模型检测、基于冲突模式的匹配和基于因果时钟图的循环依赖搜索。最后两种方法还可以定位到需求的最小错误集，方法经评估，适用于大规模系统。

嘉宾简介

陈小红

嘉宾简介：陈小红副教授，需求的形式化建模与验证专家，长期从事基于环境建模的需求工程方法，在环境建模以及基于环境的需求的形式化建模与验证方向有着独特的建树，先后在基于自然语言的形式化、基于半形式化语言的形式化及验证方面形成了系列方法，包括：针对复杂需求提出了基于场景的需求自动分解以及基于因果关系的问题约减方法，基于自动分解的组合验证方法，在系统级和配置项级进行验证；针对安全需求提出了模式语言，用于将自然语言需求形式化，提出了基于SMT的需求形式化验证方法，定义了形式化语言CCSL的图化方法，并由此定义基于图搜索的循环依赖、实时一致性验证，适用于大规模系统需求。该系列方法已经成功应用在轨道交通、航空航天等安全攸关领域。她经常在国内外需求工程、软件工程会议上发表演讲，并受邀担任RE2020会议的形式化验证workshop的主题报告人。