软件学报

作者：刘筱珊，袁正恒，陈小红，陈铭松，刘静，周庭梁

单位：刘筱珊，上海市高可信计算重点实验室(华东师范大学), 上海 20006211,袁正恒，上海市高可信计算重点实验室(华东师范大学), 上海 20006202,陈小红，上海市高可信计算重点实验室(华东师范大学), 上海 20006203,陈铭松，上海市高可信计算重点实验室(华东师范大学), 上海 20006204,刘静，上海市高可信计算重点实验室(华东师范大学), 上海 20006205,周庭梁，卡斯柯信号有限公司, 上海 20007106

关键词：区域控制器;安全需求建模;自动验证;需求分解;组合验证

基金：国家重点研发计划（2018YFB2101300）；国家自然科学基金（61332008，61872147，61572195，61802251）；上海市经济和信息化委员会专项资金（160306）

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

来源：2020年第5期

《软件学报》期刊编辑部

查看软件学报杂志2020年第5期