计算机工程

作者：赵大地, 王恪铭

单位：1. 西南交通大学信息科学与技术学院, 四川 成都 6117562. 西南交通大学计算机与人工智能学院, 四川 成都 6117563. 西南交通大学系统可信性自动验证国家地方联合实验室, 四川 成都 611756

关键词：软件功能安全,形式化方法,模型转化,SCXML状态图,B方法

基金：四川省自然科学基金(2022NSFSC0464); 成都市软科学研究项目(2023-RK00-00084-ZF)

形式化方法精确且严格, 较多应用于安全苛求系统开发, 但目前仍存在学习成本高、使用复杂、重用性低等问题。常用的非形式化状态图模型虽易于使用却缺乏严格验证。针对这些问题, 提出一种将状态图SCXML模型转译为形式化B模型的模型转化方法, 从而结合状态图的易用性降低在安全苛求软件系统开发过程中使用形式化方法的复杂度。该转译方法分为映射规则、同步语义和程序实现3个部分, 以保证自动转译后的模型自身含义与基础语义不变。在平交道口控制系统开发案例分析中, 该方法根据图元模型自动生成了对应形式化模型, 通过对形式化模型的分析改进系统在功能安全、数据安全、隐藏分支3个方面的非安全因素, 并保证从需求至模型的一致性, 证明了该方法可降低形式化方法建模难度, 提高软件系统的正确性、可靠性与安全性。

来源：2024年第11期

《计算机工程》期刊编辑部

查看计算机工程杂志2024年第11期