| 引用本文: | 吴梦丹,杨顺昆,侯展意,佘志坤,曾福萍,冀振燕.从设计到安全分析: 异构模型转换与交叉验证.软件学报,2026,37(9):3521-3556 |
| |
|
| |
|
|
| 本文已被：浏览 988次 下载 698次 |
码上扫一扫！ |
|
|
| 从设计到安全分析: 异构模型转换与交叉验证 |
|
吴梦丹1, 杨顺昆1, 侯展意1, 佘志坤2, 曾福萍1, 冀振燕3
|
|
1.北京航空航天大学 可靠性与系统工程学院, 北京 100191;2.北京航空航天大学 数学科学学院, 北京 100191;3.北京交通大学 网络空间安全学院, 北京 100044
|
|
| 摘要: |
| 在复杂软件系统开发过程中, 设计阶段与验证阶段的有效衔接是确保系统可靠性和功能正确性的关键. 然而, 设计工具与验证工具在建模语言、语义和数据结构上的异构性, 易导致模型转换语义不一致、工具链互操作性不足以及验证覆盖不充分. 为解决上述挑战, 提出一种基于统一中间表示的分层转换与多重交叉验证机制. 该机制以设计模型为起点, 结合系统理论过程分析(systems-theoretic process analysis, STPA)开展危险分析与不安全控制行为识别, 提炼安全约束, 并与既有的功能、时间和安全属性进行互补校验. 随后, 构建设计模型到统一中间表示(unified intermediate representation, UIR)的映射, 在统一语法与语义域中形式化描述结构、行为、时序与安全约束, 并据此给出覆盖上述要素的分层转换规则及其追溯性元数据. 基于UIR, 派生时序模型、逻辑模型与概率模型等互补的验证模型, 并将STPA导出的安全约束系统化映射为可验证属性, 开展源-中间-目标模型的一致性检查、时序与逻辑性验证、概率性分析以及安全约束可满足性验证等多视角交叉验证. 以自动驾驶汽车控制系统以及多域协同无人机控制系统为例的实际案例结果表明, 所提方法提高了验证的覆盖度与准确性, 增强了转换与验证过程的可追溯性, 为复杂系统的安全驱动开发提供了一条一致且可证的技术路径. |
| 关键词: 安全风险分析 统一中间表示 模型转换 多重交叉验证 |
| DOI：10.13328/j.cnki.jos.007605 |
| 分类号:TP311 |
| 基金项目:国家重点研发计划(2022YFA1005102) |
|
| From Design to Safety Analysis: Heterogeneous Model Transformation and Cross-validation |
|
WU Meng-Dan1, YANG Shun-Kun1, HOU Zhan-Yi1, SHE Zhi-Kun2, ZENG Fu-Ping1, JI Zhen-Yan3
|
|
1.School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China;2.School of Mathematical Sciences, Beihang University, Beijing 100191, China;3.School of Cyberspace Science and Technology, Beijing Jiaotong University, Beijing 100044, China
|
| Abstract: |
| In the development of complex software systems, effective integration between the design phase and the verification phase is crucial for ensuring system reliability and functional correctness. However, heterogeneity in modeling languages, semantics, and data structures across design and verification tools often leads to semantic inconsistencies during model transformation, insufficient toolchain interoperability, and inadequate verification coverage. To address these challenges, this study proposes a layered transformation and multi-perspective cross-verification mechanism based on a unified intermediate representation (UIR). Starting from the design model, systems-theoretic process analysis (STPA) is applied to conduct hazard analysis and identify unsafe control actions, from which safety constraints are extracted and cross-checked against existing functional, timing, and safety properties. Subsequently, a mapping from the design model to the UIR is constructed, and the structure, behavior, timing, and safety constraints are formally specified within a unified syntactic and semantic domain. On this basis, layered transformation rules, together with traceability metadata, are defined to cover the above elements. Based on the UIR, complementary verification models, such as temporal, logical, and probabilistic models, are derived, and the safety constraints produced by STPA are systematically translated into verifiable properties. Multi-perspective cross-verification is then conducted, including consistency checking among source, intermediate, and target models, temporal and logical property verification, probabilistic analysis, and satisfiability checking of safety constraints. Case studies on an autonomous vehicle control system and a multi-domain collaborative unmanned aerial vehicle (UAV) control system demonstrate that the proposed method improves verification coverage and accuracy, enhances traceability throughout transformation and verification, and provides a consistent and provable technical pathway for safety-driven development of complex systems. |
| Key words: safety risk analysis unified intermediate representation (UIR) model transformation multi-perspective cross-verification |
|
|
|
|
