计算机科学

计算机科学 ›› 2026, Vol. 53 ›› Issue (5): 367-375.doi: 10.11896/jsjkx.251200184

• 计算机体系结构 • 上一篇    下一篇

高可靠嵌入式软件的运行时验证方法

刘嘉乐1, 何冬梅1, 刘洪标2, 潘广宇1, 关永1, 王瑞1, 刘波2   

  1. 1 首都师范大学信息工程学院 北京 100048
    2 北京控制工程研究所 北京 100094
  • 收稿日期:2025-12-29 修回日期:2026-03-23 发布日期:2026-05-08
  • 通讯作者: 刘波(liub@bice.org.cn)
  • 作者简介:(ljl15140949762@163.com)

High-reliability Embedded Software Runtime Verification Method

LIU Jiale1, HE Dongmei1, LIU Hongbiao2, PAN Guangyu1, GUAN Yong1, WANG Rui1, LIU Bo2   

  1. 1 School of Information Engineering, Capital Normal University, Beijing 100048, China
    2 Beijing Institute of Control Engineering, Beijing 100094, China
  • Received:2025-12-29 Revised:2026-03-23 Online:2026-05-08
  • About author:LIU Jiale,born in 2001,postgraduate.Her main research interest is runtime verification.
    LIU Bo,born in 1977,Ph.D,research fellow.His main research interest is spaceborne computer architecture.

PDF (PC)

229

摘要： 高可靠嵌入式软件广泛部署于航空航天、工业控制、车载系统等安全攸关领域,其运行环境往往伴随极端温度波动、电磁干扰、高能粒子辐射等严苛条件,易引发数据位翻转、数据位错等硬件级异常,导致系统功能失效甚至引发重大安全事故。为提升高可靠嵌入式软件的运行时安全性与可靠性,提出一种面向高可靠嵌入式软件的运行时验证方法。首先,对目标程序开展静态分析,提取指令间的跳转依赖关系并构建指令控制流先验信息表;其次,设计轻量级监控模块,实时捕获程序运行时总线的指令流数据,同时通过验证单元结合先验信息表完成运行时指令序列的正确性校验;最后,基于 FPGA 平台实现该验证框架,并开展实验验证。实验结果表明,所提方法能够有效保障高可靠嵌入式软件的运行正确性,且在资源开销与验证延迟方面满足嵌入式场景的约束要求。

关键词: 高可靠嵌入式软件, 运行时验证, 程序正确性, 监控器, 硬件监控

Abstract: High-reliability embedded software is widely deployed in safety-critical domains such as aerospace,industrial control,and automotive systems,often operating under harsh conditions including extreme temperature fluctuations,electromagnetic interference,and high-energy particle radiation.These conditions can easily trigger hardware-level anomalies like single-event upsets and data bit flips,leading to system functional failures or even major safety incidents.To enhance the runtime safety and reliability of high-reliability embedded software,this paper proposes a runtime verification method tailored for such software.Firstly,it performs static analysis on the target program to extract jump dependencies between instructions and constructs a priori instruction control flow information table.Secondly,it designs a lightweight monitoring module to capture real-time instruction flow data from the program’s bus,while verifying the correctness of the runtime instruction sequence through validation units combined with the a priori information table.Finally,it implements the verification framework on an FPGA platform and conducts experimental validation.The results demonstrate that the proposed method effectively ensures the correctness of high-reliability embedded software while meeting the resource constraints and verification latency requirements of embedded scenarios.

Key words: High-reliability embedded software, Runtime verification, Program correctness, Monitor, Hardware monitoring

中图分类号: 

  • TP311
[1]GAI J L,MI Y,MA B B.A Survey on Redundant Fault-tolerant Technology of Liquid Rocket Engine Fault Diagnosis System[J].Computer Measurement & Control,2024,32(8):1-7.
[2]LI Y,HU Y M,ZENG X Y.A Three-Module Redundancy Soft Error Protection Technology for Cost-Effective Commercial Space Satellites:The Practice of Approximate Computing[J].Journal of Electronics & Information Technology,2024,46(5):1604-1612.
[3]WANG J,HUANG Y,CHEN C,et al.Software testing withlarge language models:Survey,landscape,and vision[J].IEEE Transactions on Software Engineering,2024,50(4):911-936.
[4]KUMAR S.Reviewing software testing models and optimization techniques:an analysis of efficiency and advancement needs[J].Journal of Computers,Mechanical and Management,2023,2(1):32-46.
[5]SUN XX,CHEN Z.Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving[J].Computer Science,2021,48(1):268-272.
[6]BEYER D,LEE N Z,WENDLER P.Interpolation and SAT-based model checking revisited:Adoption to software verification[J].Journal of Automated Reasoning,2025,69(1):5.
[7]CHEN Z,MOTET G.Nevertrace claims for model checking[C]//International SPIN Workshop on Model Checking of Software.Berlin:Springer,2010:162-179.
[8]LEUCKER M,SCHALLHART C.A brief account of runtime verification[J].The Journal of Logic and Algebraic Programming,2009,78(5):293-303.
[9]CHEN Z,WANG Z,ZHU Y,et al.Parametric Runtime Verification of C Programs[C]//International Conference on Tools andAlgorithms for the Construction and Analysis of Systems.Berlin:Springer,2016:299-315.
[10]MEREDITH P O N,JIN D,GRIFFITH D,et al.An overview of the MOP runtime verification framework[J].International Journal on Software Tools for Technology Transfer,2012,14(3):249-289.
[11]MACNAMEE C,HEFFERNAN D.On-Chip Instrumentationfor Runtime Verification in Deeply Embedded Processors[C]//2015 IEEE Computer Society Annual Symposium on VLSI.IEEE,2015:374-379.
[12]BU L,DONG W,SHAN Y X.Current Status and Prospects of Runtime Software Verification and Monitoring[J].Science and Technology Foresight,2023,2(1):62-77.
[13]LIU D M.Research on Runtime Verification Technology Based on PPTL3[D].Xi’an:Xidian University,2017.
[14]YANG H G,SUN J B,WANG W.An Overview to FPGA Device Design Technologies[J].Journal of Electronics & Information Technology,2010,32(3):714-727.
[15]ZHAO P,CHENG G,ZHAO D Y.Survey on FPGA-based High-performance Programmable Data Plane[J].Ruan Jian Xue Bao,2023,34(11):5330-5354.
[16]SOLET D,PILLEMENT S,BÉCHENNEC J L,et al.Hw-based architecture for runtime verification of embedded software on SoPC systems[C]//Proceedings of 2018 NASA/ESA Confe-rence on Adaptive Hardware and Systems (AHS).2018.
[17]SOLET D,BÉCHENNEC J L,BRIDAY M,et al.A Study in Specification and Hardware Runtime Verification of Critical Embedded Software[J].IEEE Transactions on Dependable and Secure Computing,2025,22(3):2258-2269.
[18] WAHAB M A,COTRET P,NASR ALLAH M,et al.ARMHEx:A hardware extension for DIFT on ARM-based SoCs[C]//Proceedings of International Conference on Field Programmable Logic and Applications (FPL).2017.
[19]LESNIAK F,ANANTHARAJAIAH N,HARBAUM T,et al.Non-Intrusive Runtime Monitoring for Manycore Prototypes[C]//Proceedings of the DroneSE and RAPIDO:System Engineering for Constrained Embedded Systems.2023.
[20]HAVELUND K.Using runtime analysis to guide model checking of Java programs[C]//International SPIN Workshop on Model Checking of Software.Berlin:Springer,2000:245-264.
[21]HAVELUND K,ROŞU G.Monitoring java programs with java pathexplorer[J].Electronic Notes in Theoretical Computer Science,2001,55(2):200-217.
[22]LUO N L.Research on Software Runtime Verification Method Based on LTL Three-Valued Semantics[D].Harbin:Harbin Engineering University,2017.
[23]ZHANG X,DONG W,QI Z C.Conflict detection in runtime ve-rification based on AOP[J].Journal of Software,2011,22(6):1224-1235.
[24]SEN K,ROŞU G.Generating optimal monitors for extendedregular expressions[J].Electronic Notes in Theoretical Computer Science,2003,89(2):226-245.
[25]ALLAN C,AVGUSTINOV P,CHRISTENSEN A S,et al.Adding trace matching with free variables to AspectJ[J].ACM SIGPLAN Notices,2005,40(10):345-364.
[26]LU X,DUAN Z H,TIAN C.Satisfiability checking of two-dimensional logic PPTLSL[J].Journal of Software,2016,27(3):670-681.
[27]ANGLUIN D,FISMAN D.Learning regular omega languages[J].Theoretical Computer Science,2014,650:57-72.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市两江新区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发