Computer Science ›› 2026, Vol. 53 ›› Issue (5): 367-375.doi: 10.11896/jsjkx.251200184

• Computer Architecture • Previous Articles     Next Articles

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 Published: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.

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

CLC Number: 

  • 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.
[1] SHI Junnan, CHEN Zemao, ZHANG Liqiang. Automatic Attack Path Discovery Method for Substation Remote Monitoring Network [J]. Computer Science, 2025, 52(12): 339-350.
[2] MAO Ruiqi, CHEN Zhe. Lightweight Memory Safety Runtime Detection Method Combined with Static Analysis [J]. Computer Science, 2025, 52(11A): 241100060-8.
[3] LI Xiaogeng, HAN Xiao, XIAO Haiyi. Cooperative Defense Method for Network Space Object of Power Monitoring System [J]. Computer Science, 2025, 52(11A): 241200158-7.
[4] JIANG Yakun, LIN Xu. Intrusion Detection Method for Power Monitoring System Based on Multi-source Network Data [J]. Computer Science, 2025, 52(11A): 241200157-7.
[5] ZHOU Zheng, CHEN Chen, WANG Song, SONG Xiaofan. Research on Timeliness of Information Flow of Main and Auxiliary Business of Plant and StationUnder Comprehensive Monitoring [J]. Computer Science, 2025, 52(11A): 241100111-6.
[6] LU Dongsheng, LONG Hua. Method for Homologous Spectrum Monitoring Data Identification Based on Spectrum SIFT [J]. Computer Science, 2024, 51(6A): 230300177-7.
[7] YAN Xinyu, HUANG Zengfeng. Robust Distributed Monitoring Algorithm Under Limited Interference [J]. Computer Science, 2024, 51(11A): 240200050-7.
[8] YAO Xi. Grid-based Tracking Method for Hydrographic Mapping UAV [J]. Computer Science, 2023, 50(6A): 220300023-7.
[9] BING Ying’ao, WANG Wenting, SUN Shengze, LIU Xin, NIE Qigui, LIU Jing. Network Reliability Analysis of Power Monitoring System Based on Improved Fuzzy ComprehensiveEvaluation Method [J]. Computer Science, 2023, 50(6A): 220400293-7.
[10] XUE Fenghao, JIANG Haibo, TANG Dan. Review of Deep Learning Applications in Healthcare [J]. Computer Science, 2023, 50(4): 1-15.
[11] CHEN Jinjie, HE Chao, XIAO Xiao, LEI Yinjie. Optical Performance Monitoring Method Based on Fine-grained Constellation Diagram Recognition [J]. Computer Science, 2023, 50(4): 220-225.
[12] YANG Xiao, WANG Xiang-kun, HU Hao, ZHU Min. Survey on Visualization Technology for Equipment Condition Monitoring [J]. Computer Science, 2022, 49(7): 89-99.
[13] LI Xiao-dong, YU Zhi-yong, HUANG Fang-wan, ZHU Wei-ping, TU Chun-yu, ZHENG Wei-nan. Participant Selection Strategies Based on Crowd Sensing for River Environmental Monitoring [J]. Computer Science, 2022, 49(5): 371-379.
[14] FENG Lei, FENG Li, FANG Fang, GUO Jin-song, PAN Jiang, YU You, CHEN Yu. Improved Water Quality Remote Sensing Monitoring Algorithms Based on Multilayer Convolutional Neural Network [J]. Computer Science, 2022, 49(11A): 210200160-5.
[15] YUAN Yu-kun, LI Gang, ZHAO Zhi-xiang, XU Li. Research on Factors Affecting Stock Inflection Point Based on Machine Learning Algorithms [J]. Computer Science, 2021, 48(6A): 165-168.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!