区域控制器的安全需求建模与自动验证

• 作者: 刘筱珊 刘静 周庭梁 袁正恒 陈小红 陈铭松
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 区域控制器 安全需求建模 自动验证 需求分解 组合验证
• 年，卷（期）: 2020,（5）
• 所属期刊栏目: 系统软件构造与验证技术专题
• 页码范围: 1374-1391
• 页数: 18页
• 分类号: TP311
• 字数: 15087字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005952

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周庭梁		16	68	4.0	8.0