基于模型的系统验证：理论框架、关键技术及未来展望

doi:10.16182/j.issn1004731x.joss.25-0797

系统仿真学报 ›› 2026, Vol. 38 ›› Issue (4): 829-854.doi: 10.16182/j.issn1004731x.joss.25-0797

• 专家约稿 • 下一篇

基于模型的系统验证：理论框架、关键技术及未来展望

孙波¹, 任羿², 王偲霖³, 刘奇⁴, 李志栋¹

^1.北京空间飞行器总体设计部，北京 100094
^2.北京航空航天大学，北京 100191
^3.哈尔滨工程大学，黑龙江哈尔滨 150001
^4.苏州同元软控信息技术有限公司，江苏苏州 215000

收稿日期:2025-08-22 修回日期:2025-11-07 出版日期:2026-04-20 发布日期:2026-04-22
通讯作者: 任羿
第一作者简介:孙波(1974-)，男，研究员，博士，研究方向为数字试验与测试，装备健康管理，智能装备可信性测试与评估。
孙波研究员(博士生导师)，毕业于北京航空航天大学，获计算机软件博士学位，现任中国航天科技集团有限公司第五研究院总体部研究员，中国仿真学会理事，中国仿真学会数字试验与测试专业委员会主任委员，中国造船工程学会舰船保障学术委员会委员、指挥控制协会集群智能与协同控制专业委员会委员。从事基于模型的测试验证、数字化试验与测试、健康管理等方面的研究工作。出版专著一部。
任羿北京航空航天大学蓝天杰出教授(二级)，可靠性系统工程学科方向带头人。入选国家级领军人才计划，兼任中国仿真学会理事、中国仿真学会数字试验与测试分委会副主任、系统仿真学报编委。发表SCI论文100余篇，授权发明专利80余项，主编中英文专著3部，主持多项国家级重大重点科研项目。获国家科技进步二等奖1项、省部级科技进步一等奖4项、集体荣获(带头人)省部级科技创新团队奖1项。

Model-based System Verification: Theoretical Framework, Key Technologies, and Future Prospects

Sun Bo¹, Ren Yi², Wang Silin³, Liu Qi⁴, Li Zhidong¹

^1.Beijing Institute of Spacecraft System Engineering, Beijing 100094, China
^2.Beihang University, Beijing 100191, China
^3.Harbin Engineering University, Harbin 150001, China
^4.Suzhou Tongyuan Soft Control Information Technology Co. , Ltd. , Suzhou 215000, China

Received:2025-08-22 Revised:2025-11-07 Online:2026-04-20 Published:2026-04-22
Contact: Ren Yi

摘要/Abstract

摘要：

为解决传统的系统验证方法在效率、覆盖度和可追溯性等方面面临的严峻挑战，提出基于模型的系统验证(model-based system verification，MBSV)，将验证活动深度融入基于模型的系统工程模型体系及其演化过程。给出了MBSV的构建逻辑，提出一种以系统建模语言(system modeling language，SysML)为基础，融合需求、结构、行为与约束的多视图统一验证建模策略。论述了旨在提升验证效率的路径代表性选择与等价类约简算法、测试路径搜索原理，以及基于RL的路径智能搜索机制；描述了从抽象路径到可执行测试用例的自动化生成流程，探讨了基于功能模型单元与仿真平台SDK的双通道自动化执行机制，以实现验证任务在异构仿真环境中的无缝部署与闭环反馈。展望了MBSV未来发展的重点方向。

关键词: 基于模型的系统验证, 基于模型的系统工程, 系统建模语言, 测试路径搜索, 测试路径约简, 测试用例自动生成, 测试仿真平台, 姿态确定与控制系统

Abstract:

Traditional system verification methods face significant challenges in terms of efficiency, coverage, and traceability. To address these issues, this paper introduced model-based system verification (MBSV), which deeply integrated verification activities within the model-based systems engineering model system and evolution process. It presented the foundational logic of MBSV and proposed a multi-view unified verification modeling strategy based on system modeling language (SysML), integrating requirements, structure, behavior, and constraints. The paper discussed the algorithms for selecting representative paths and reducing equivalent classes to enhance verification efficiency, the principles of test path search, as well as the intelligent path search mechanism based on RL. It detailed the automated generation process for transforming abstract paths into executable test cases and discussed a dual-channel automated execution mechanism based on functional mock-up units and simulation platform SDKs to enable the seamless deployment and closed-loop feedback of verification tasks within heterogeneous simulation environments. The paper outlined future research directions for MBSV.

Key words: model-based system verification, model-based systems engineering, system modeling language, test path search, test path reduction, automated test case generation, test simulation platform, attitude determination and control system

中图分类号:

TP391

孙波,任羿,王偲霖等 . 基于模型的系统验证：理论框架、关键技术及未来展望[J]. 系统仿真学报, 2026, 38(4): 829-854.

Sun Bo,Ren Yi,Wang Silin,et al . Model-based System Verification: Theoretical Framework, Key Technologies, and Future Prospects[J]. Journal of System Simulation, 2026, 38(4): 829-854.

图/表 10

图1

图2

表1

术语与符号表

符号	术语/名称	形式化定义/说明
$M = (S, X, U, T, O)$	系统模型	状态集 $S$ 、可观测量 $X$ 、输入 $U$ 、状态转移 $T : S × U → S$ 、观测 $O : S → X$
$S$	状态空间	系统内部配置/变量的笛卡尔积
$X$	可观测空间	由观测映射获得的输出量
$U$	输入空间	可注入的控制/扰动变量集合
$T$	状态转移	$S k + 1 = T (s k, u k)$
$O$	观测映射	$y k = O (s k)$
$Γ$	语义映射	SysML图元 $→$ {约束，断言}的规范化映射
$G = (V, E, Λ)$	约束耦合状态图(CCSD)	顶点 $V$ 、有向边 $E$ 、边标注 $Λ (e) = (g u a r d, i n p u t_d o m a i n, a s s e r t)$
$π = (v 0, v 1, ⋯, v L)$	路径	图G上的顶点序列；可行性受守卫与输入域约束
P_cand， $P r$	候选路径集/代表性路径集	生成的全部候选路径集/经选择后的代表性路径集
$σ (π)$	路径签名	$h a s h (s t a t e_s e q, g u a r d s, a s s e r t s)$
$p G$	泛化路径	多条路径在 $R i n p$ 、 $R a s s e r t$ 达到阈值时形成的泛化路径
$R i n p$ ， $R a s s e r t$	输入域重叠率/断言一致率	$[0,1]$ 上的相似性度量
$~$	结构等价关系	$π a ~ π b ⇔ σ (π a) = σ (π b)$ 且共享关键子图
$τ u, τ a$	合并阈值	触发泛化/合并的下限
$U π$	路径可行域	$∩ e ∈ π i n p u t_d o m a i n e$
$C s t r u c t$	结构覆盖	状态/转移/判定－条件等覆盖率
$T (π)$	用例序列	$(s k, u k, α k) k = 0 L$ ，其中， $α k ⊆ Φ$
$g u a r d e$	守卫条件	使能边e的逻辑条件
$I s e q$	输入序列	来自输入空间的一系列有序输入
$S s e q$	状态轨迹	系统在特定 $I s e q$ 作用下所经历的状态序列
$ϵ a t t$	指向精度阈值	姿态指向误差RMS允许上限
$ϵ v o t e d$	冗余表决误差阈值	冗余“三取二”表决后姿态误差RMS的允许上限
$σ m a x$	最大超调量	模式切换过程中姿态指向误差的最大允许超调量
$T s e t t l e$	稳定时间上限	姿态指向误差收敛并保持在阈值内的最大允许时间
$T d e t e c t$	故障检测时间上限	FDIR从故障发生到完成识别的最大允许时间
$T u n l o a d$	卸载时间上限	动量轮从进入饱和到恢复至安全区间的最大允许时间
$H m a x$	饱和角动量阈值	判定动量轮进入饱和状态的角动量阈值
MM	动量管理子系统	Momentum Management子系统，负责监视与卸载轮系角动量

表1

图3

表2

图4

图5

图6

图7

图8

参考文献 37

[1]	Piaszczyk C. Model Based Systems Engineering with Department of Defense Architectural Framework[J]. Systems Engineering, 2011, 14(3): 305-326.
[2]	Morkevicius A, Aleksandraviciene A, Strolia Z. System Verification and Validation Approach Using the MagicGrid Framework[J]. INSIGHT, 2023, 26(1): 51-59.
[3]	孙波, 郑凯. 数字试验测试技术研究现状、挑战与展望[J]. 系统仿真学报, 2025, 37(8): 1885-1906.
	Sun Bo, Zheng Kai. Digital Testing and Evaluation: Current Status, Challenges, and Prospects[J]. Journal of System Simulation, 2025, 37(8): 1885-1906.
[4]	Li H, Lu P. Research on Model-based Reliability Verification Technique for Civil Aircraft [C]//Proceedings of 2023 Global Reliability and Prognostics and Health Management Conference (PHM-Hangzhou). Piscataway: IEEE, 2023: 1-6. DOI: 10.1109/PHM-Hangzhou58797.2023.10482711 .
[5]	Cederbladh Johan, Cicchetti Antonio, Suryadevara Jagadish. Early Validation and Verification of System Behaviour in Model-based Systems Engineering: A Systematic Literature Review[J]. ACM Transactions on Software Engineering and Methodology, 2024, 33(3): 81.
[6]	于国斌. 深空探测任务协同的系统工程方法应用及趋势[J]. 深空探测学报(中英文), 2021, 8(4): 407-415.
	Yu Gubin. Application and Trend of Model-based Systems Engineering Methods for Deep Space Exploration Mission[J]. Journal of Deep Space Exploration, 2021, 8(4): 407-415.
[7]	Ramirez C, Thompson A. Verification and Validation Test Framework Using a Model-based Systems Engineering Approach[J]. INCOSE International Symposium, 2023, 33(1): 1091-1116.
[8]	Madni A M. MBSE Testbed for Rapid, Cost-effective Prototyping and Evaluation of System Modeling Approaches[J]. Applied Sciences, 2021, 11(5): 2321.
[9]	Tian Ye, Yin Beibei, Li Chenglong. A Model-based Test Cases Generation Method for Spacecraft Software[C]//2021 8th International Conference on Dependable Systems and Their Applications (DSA). Piscataway: IEEE, 2021: 373-382.
[10]	Bartocci Ezio, Mariani Leonardo, Nickovic Dejan, et al. Signal Feature Coverage and Testing for CPS Dataflow Models[J]. ACM Transactions on Software Engineering and Methodology, 2025, 34(7): 199.
[11]	Su Zhuo, Yu Zehong, Wang Dongyan, et al. Test Case Generation for Simulink Models Using Model Fuzzing and State Solving[C]//Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. New York: Association for Computing Machinery, 2024: 117-128.
[12]	陆涵, 张霖, 王昆玉, 等. 装备数字孪生可信评估框架研究[J]. 系统仿真学报, 2023, 35(7): 1455-1471.
	Lu Han, Zhang Lin, Wang Kunyu, et al. A Framework on Equipment Digital Twin Credibility Assessment[J]. Journal of System Simulation, 2023, 35(7): 1455-1471.
[13]	胡军, 张维珺, 李宛倩. 面向需求的安全关键系统形式化建模与验证方法研究[J]. 计算机工程与科学, 2019, 41(8): 1426-1433.
	Hu Jun, Zhang Weijun, Li Wanqian. A Requirement Oriented Formal Modeling and Verification Method for Safety Critical Systems[J]. Computer Engineering & Science, 2019, 41(8): 1426-1433.
[14]	肖思慧, 刘琦, 黄滟鸿, 等. 基于SysML的机载软件分层精化建模与验证方法[J]. 软件学报, 2022, 33(8): 2851-2874.
	Xiao Sihui, Liu Qi, Huang Yanhong, et al. Hierarchical Refined Modeling and Verification Method of Airborne Software Using SysML[J]. Journal of Software, 2022, 33(8): 2851-2874.
[15]	牛浩田, 马存宝, 韩佩, 等. 面向航电系统任务安全性的形式化建模与验证[J]. 系统工程与电子技术, 2023, 45(5): 1553-1569.
	Niu Haotian, Ma Cunbao, Han Pei, et al. Formal Modeling and Verification for Mission Safety of Avionics System[J]. Systems Engineering and Electronics, 2023, 45(5): 1553-1569.
[16]	Molnár Vince, Graics Bence, Vörös András, et al. Towards the Formal Verification of SysML v2 Models[C]//Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems. New York: Association for Computing Machinery, 2024: 1086-1095.
[17]	李彦瑞, 杨春节, 张瀚文, 等. 流程工业数字孪生关键技术探讨[J]. 自动化学报, 2021, 47(3): 501-514.
	Li Yanrui, Yang Chunjie, Zhang Hanwen, et al. Discussion on Key Technologies of Digital Twin in Process Industry[J]. Acta Automatica Sinica, 2021, 47(3): 501-514.
[18]	Löcklin Andreas, Müller Manuel, Jung Tobias, et al. Digital Twin for Verification and Validation of Industrial Automation Systems-a Survey[C]//2020 25th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). Piscataway: IEEE, 2020: 851-858.
[19]	陶飞, 高鹏飞, 张辰源, 等. 数字试验测试验证: 理论、关键技术及应用探索[J]. 机械工程学报, 2024, 60(15): 227-254.
	Tao Fei, Gao Pengfei, Zhang Chenyuan, et al. D-ETV: Digital Experiment, Testing and Verification[J]. Journal of Mechanical Engineering, 2024, 60(15): 227-254.
[20]	杨波, 吴际, 徐珞, 等. 一种软件测试需求建模及测试用例生成方法[J]. 计算机学报, 2014, 37(3): 522-537.
	Yang Bo, Wu Ji, Xu Luo, et al. An Approach of Modeling Software Testing Requirements and Generating Test Cases[J]. Chinese Journal of Computers, 2014, 37(3): 522-537.
[21]	王鹏, 岳舒婷, 张帆, 等. 基于有限谓词追踪的民机系统需求一致性检查方法[J]. 系统工程与电子技术, 2024, 46(1): 205-218.
	Wang Peng, Yue Shuting, Zhang Fan, et al. Requirement Consistency Checking Method for Civil Aircraft Systems Based on Finite Predicate Tracing[J]. Systems Engineering and Electronics, 2024, 46(1): 205-218.
[22]	Spangelo S C, Kaslow D, Delp C, et al. Applying Model Based Systems Engineering (MBSE) to a Standard CubeSat[C]//2012 IEEE Aerospace Conference. Piscataway: IEEE, 2012: 1-20.
[23]	Cao Yue, Liu Yusheng, Qin Xujia. A Hybrid Approach to System Verification in Early Design for Complex Mechatronic Systems Based on Formal Functional Semantics[J]. Advanced Engineering Informatics, 2023, 58: 102201.
[24]	Izukura Sayaka, Yanoo Kazuo, Osaki Takao, et al. Applying a Model-based Approach to IT Systems Development Using SysML Extension[C]//Proceedings of the ACM/IEEE 14th International Conference on Model Driven Engineering Languages and Systems. Berlin: Springer Berlin Heidelberg, 2011: 563-577.
[25]	Apvrille Ludovic, Pierre de Saqui-Sannes, Hotescu Oana, et al. SysML Models Verification Relying on Dependency Graphs[C]//10th International Conference on Model-Driven Engineering and Software Development. Setúbal: Science and Technology Publications, Lda, 2022: 174-181.
[26]	Phillips I, Kenley C R. System Verification via Model-checking: A Case Study of an Autonomous Multi-differential Drive Robot[J]. INCOSE International Symposium, 2023, 17(1): 17-31.
[27]	He J, Sivanrupan G, Tsankov P, et al. Learning to Explore Paths for Symbolic Execution [C]∥ Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS '21). New York: Association for Computing Machinery (ACM), 2021: 2526-2540. DOI: 10.1145/3460120.3484813 .
[28]	Khan M K. Reinforcement Learning-based Test Case Generation with Test Suite Prioritization for Android Application Testing[D]. Denton: University of North Texas, 2023.
[29]	Corradini Davide, Montolli Zeno, Pasqua Michele, et al. DeepREST: Automated Test Case Generation for REST APIs Exploiting Deep Reinforcement Learning[C]//2024 39th IEEE/ACM International Conference on Automated Software Engineering (ASE). Piscataway: IEEE, 2024: 1383-1394.
[30]	Simon Thrane Hansen, Cláudio Ângelo Gonçalves Gomes, Najafi Masoud, et al. The FMI 3.0 Standard Interface for Clocked and Scheduled Simulations[J]. Electronics, 2022, 11(21): 3635.
[31]	Hecht M, Chen J, Pugliese-Rosillo G. Verification and Validation of SysML Models[C]//2021 IEEE Aerospace Conference. Piscataway: IEEE, 2021: 1-6.
[32]	Lops A, Narducci F, Ragone A, et al. A System for Automated Unit Test Generation Using Large Language Models and Assessment of Generated Test Suites[C/OL]//2025 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). 2025: 29-36
[33]	Yang L, Yang C, Gao S, et al. On the Evaluation of Large Language Models in Unit Test Generation [C]∥ Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024). New York: Association for Computing Machinery (ACM), 2024: 1607-1619. DOI: 10.1145/3691620.3695529 .
[34]	Zhang W, Cockburn C, Henshaw M, et al. MBSE Co-Pilot: A Research Roadmap[J]. Systems Engineering, 2025, 0: 1-14.
[35]	王自力, 高鋆添, 杨德真, 等. 智能系统可靠性仿真测试与验证技术:前沿进展与挑战[J]. 系统仿真学报, 2025, 37(7): 1583-1606.
	Wang Zili, Gao Juntian, Yang Dezhen, et al. Reliability Simulation Testing and Verification Technologies for Intelligent Systems: Frontiers, Progress, and Challenges[J]. Journal of System Simulation, 2025, 37(7): 1583-1606.
[36]	Perisic Ana, Perisic Branko. Digital Twins Verification and Validation Approach Through the Quintuple Helix Conceptual Framework[J]. Electronics, 2024, 13(16): 3303.
[37]	陶飞, 马昕, 张辰源, 等. 数字试验测试验证标准体系[J]. 计算机集成制造系统, 2025, 31(1): 1-19.
	Tao Fei, Ma Xin, Zhang Chenyuan, et al. A Standard System for Digital Experiment, Testing, and Validation(D-ETV)[J]. Computer Integrated Manufacturing Systems, 2025, 31(1): 1-19.

UTP概念(OMG标准)	描述	MBSV的CCSD 等价/类比概念	映射与理由
TestCase(测试用例)	用于验证特定需求的测试过程规约	从CCSD模型生成一条完整的代表性路径	路径定义了状态和转移的序列，构成了测试过程的核心逻辑
CreateStimulusAction (创建刺激动作)	指示测试器向被测系统提交一个刺激的动作	三元组中的I	I定义了触发该状态转移的有效输入集合，功能上等同于测试刺激
ExpectResponseAction/ CheckPropertyAction	指示测试器观察一个预期响应或检查系统内部属性的动作	三元组中的A	A定义了在转移完成后必须成立的条件，代表了对系统响应或状态的预期和检查
前/后置条件 (Pre/Post Conditions)	测试步骤执行前后必须满足的逻辑条件	g充当了该测试步骤即状态转移的前置条件	g明确定义了使能该测试步骤所必需的系统状态
Verdict (判定结果：pass/fail)	对测试用例执行结果评估	在执行过程中对路径上所有A的评估结果	如果路径上所有A中的断言都成立，判定为“pass”，否则为“fail”

基于模型的系统验证：理论框架、关键技术及未来展望

Model-based System Verification: Theoretical Framework, Key Technologies, and Future Prospects

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 10

参考文献 37

相关文章 7

编辑推荐

Metrics

本文评价

[1]	彭莱春阳, 叶飞, 郭晓明, 周靖林. X语言仿真大模型：体系架构、关键技术与典型应用[J]. 系统仿真学报, 2026, 38(4): 869-888.
[2]	曹晞, 刘波, 苏炳志, 聂涛. 基于MBSE和VAPS的民用直升机显控系统设计与验证[J]. 系统仿真学报, 2025, 37(3): 704-717.
[3]	邢志伟, 于瑞文, 李彪, 陈肇欣. 航班地面保障过程决策支持体系建模[J]. 系统仿真学报, 2024, 36(11): 2552-2565.
[4]	古鹏飞, 张霖, 陈真, 叶俊杰. 基于X语言的起飞场景民机协同设计与仿真一体化方法[J]. 系统仿真学报, 2022, 34(5): 929-943.
[5]	张霖, 王昆玉, 赖李媛君, 任磊. 基于建模仿真的体系工程[J]. 系统仿真学报, 2022, 34(2): 179-190.
[6]	赵良玉, 叶俊杰, 何琪, 郭玮, 赵勇. 基于MBSE的民机起飞场景仿真[J]. 系统仿真学报, 2021, 33(10): 2499-2510.
[7]	迟玥, 单栋, 阎振鑫, 黑鹏. 基于模型的仿真设计在某飞控系统中的应用[J]. 系统仿真学报, 2017, 29(10): 2556-2566.