软件学报

作者：吴梦丹，杨顺昆，侯展意，佘志坤，曾福萍，冀振燕

单位：吴梦丹，北京航空航天大学 可靠性与系统工程学院, 北京 10019111,杨顺昆，北京航空航天大学 可靠性与系统工程学院, 北京 10019102,侯展意，北京航空航天大学 可靠性与系统工程学院, 北京 10019103,佘志坤，北京航空航天大学 数学科学学院, 北京 10019104,曾福萍，北京航空航天大学 可靠性与系统工程学院, 北京 10019105,冀振燕，北京交通大学 网络空间安全学院, 北京 10004406

关键词：安全风险分析;统一中间表示;模型转换;多重交叉验证

基金：国家重点研发计划(2022YFA1005102)

在复杂软件系统开发过程中,设计阶段与验证阶段的有效衔接是确保系统可靠性和功能正确性的关键.然而,设计工具与验证工具在建模语言、语义和数据结构上的异构性,易导致模型转换语义不一致、工具链互操作性不足以及验证覆盖不充分.为解决上述挑战,本文提出一种基于统一中间表示的分层转换与多重交叉验证机制.该机制以设计模型为起点,结合系统理论过程分析(STPA)开展危险分析与不安全控制行为识别,提炼安全约束,并与既有的功能、时间和安全属性进行互补校验.随后,构建设计模型到统一中间表示(UIR,Unified Intermediate Representation)的映射,在统一语法与语义域中形式化描述结构、行为、时序与安全约束,并据此给出覆盖上述要素的分层转换规则及其追溯性元数据.基于UIR,派生时序模型、逻辑模型与概率模型等互补的验证模型,并将STPA导出的安全约束系统化映射为可验证属性,开展源-中间-目标模型的一致性检查、时序与逻辑性验证、概率性分析以及安全约束可满足性验证等多视角交叉验证.以自动驾驶汽车控制系统以及多域协同无人机控制系统为例的实际案例结果表明,所提方法提高了验证的覆盖度与准确性,增强了转换与验证过程的可追溯性,为复杂系统的安全驱动开发提供了一条一致且可证的技术路径.

来源：2026年第9期

《软件学报》期刊编辑部

查看软件学报杂志2026年第9期