当前位置:首页 >> 演讲嘉宾
陈小红

演讲主题:

轨道交通系统中的需求建模与形式化验证

 

嘉宾简介:

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

 

演讲简介:

轨道交通区域控制器是我国轨道交通信号系统选型的主流制式——基于通信的列车控制系统的核心子系统,其突出的安全性使得安全需求的形式化验证成为一个非常重要的问题。但是区域控制器自身的复杂性以及领域知识的繁杂难以掌握,使得形式化方法很难应用到安全需求的验证中去。针对这些问题,提出一种安全需求的自动验证方法,使用半形式化的问题框架方法来建模和分解安全需求,根据需求模型自动生成安全需求的验证模型和验证性质,在此基础上自动生成验证模型的Scade语言实现,并通过Design Verifier验证器对需求进行组合验证。最后,使用某个实际案例区域控制器的一个子问题CAL_EOA进行了研究,实验结果证明了该方法的可行性与有效性。它能够自动地将安全需求模型进行组合验证,改善了验证的效率。