Current Status and Prospects of Runtime Software Verification and Monitoring

doi:10.3981/j.issn.2097-0781.2023.01.005

Science and Technology Foresight ›› 2023, Vol. 2 ›› Issue (1): 62-77.DOI: 10.3981/j.issn.2097-0781.2023.01.005

• Review and Commentary • Previous Articles Next Articles

Current Status and Prospects of Runtime Software Verification and Monitoring

BU Lei¹^,²(), DONG Wei³^,^†(), SHAN Yunxiao⁴^,⁵

1. State Key Laboratory for Novel Software Technology at Nanjing University, Nanjing 210023, China
2. Software Institute, Nanjing University, Nanjing 210023, China
3. College of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China
4. School of Artificial Intelligence, Sun Yat-sen University, Zhuhai 519082, China
5. Guangdong Key Laboratory of Big Data Analysis and Processing, Guangzhou 510275, China

Received:2023-01-06 Revised:2023-02-06 Online:2023-03-20 Published:2023-03-27
Contact: ^†

软件运行时验证与监控技术发展现状与展望

卜磊¹^,²(), 董威³^,^†(), 单云霄⁴^,⁵

1.南京大学计算机软件新技术国家重点实验室，南京 210023
2.南京大学软件学院，南京 210023
3.国防科技大学计算机学院，长沙 410073
4.中山大学人工智能学院，珠海 519082
5.广东省大数据分析与处理重点实验室，广州 510275

通讯作者: ^†
作者简介:卜磊，教授，博士研究生导师。中国计算机学会系统软件专业委员会秘书长。主要研究领域为软件工程与形式化方法，包括模型检验技术、实时混成系统、信息物理融合系统等方向。入选国家级青年人才计划、高校计算机专业优秀教师奖励计划。获NASAC青年软件创新奖、CCF-IEEE CS青年科学家奖等。电子信箱：bulei@nju.edu.cn。
董威，教授，博士研究生导师。中国计算机学会形式化方法专业委员会秘书长。主要研究方向为高可信软件技术、智能化软件开发方法。入选教育部新世纪优秀人才支持计划。获NASAC青年软件创新奖、霍英东教育基金会高等院校青年教师奖等。先后主持国家自然科学基金重大项目、国家高技术研究发展计划、国家重点基础研究发展计划和国防领域课题10余项。出版国家级规划教材2部，发表学术论文70余篇。电子信箱：wdong@nudt.edu.cn。
基金资助:
国家自然科学基金(62232008);国家自然科学基金(62172200);国家自然科学基金(62032019);江苏省前沿引领技术基础研究专项(BK20202001);广东省粤穗联合基金青年基金(2020A1515110199);深圳市基础研究项目(JCYJ20210324122203009);深圳市基础研究项目(JCYJ20180508152434975)

Abstract

Abstract:

Nowadays, many software systems are working in open, dynamic, and nondeterministic scenarios, often suffering from unexpected interference and influence. It is important to conduct runtime verification and monitoring of system behavior and adaptively make real-time responses and decisions for and exert dynamic control over each real-time situation. This paper reviews the research progress of runtime verification, monitoring, enhancement, and dynamical control in and outside China and their prospects. Meanwhile, it also explores and recommends potential future research directions from the perspectives of the understanding of system behavior, controller synthesis, full-cycle monitoring, etc.

Key words: formal modeling and verification, runtime verification, online monitoring, control synthesis

摘要：

当今社会，大量软件系统运行在开放、动态、不确定的场景中，经常受到非预期的干扰和影响，因此对系统行为进行运行时验证与监控，并针对各种实时情况做出自适应的实时响应、决策与动态调控，具有重要意义。文章从运行时验证、监控、增强及动态调控等方面对相关领域的国内外进展进行了回顾与展望，并从软件行为认知与理解、控制器生成、全生命期监控等角度对后续潜在方向进行探讨与建议。

关键词: 形式化建模与验证, 运行时验证, 在线监控, 控制生成

BU Lei, DONG Wei, SHAN Yunxiao. Current Status and Prospects of Runtime Software Verification and Monitoring[J]. Science and Technology Foresight, 2023, 2(1): 62-77.

卜磊, 董威, 单云霄. 软件运行时验证与监控技术发展现状与展望[J]. 前瞻科技, 2023, 2(1): 62-77.

Figures/Tables 2

References 110

[1]	Bertot Y, Castéran P. Interactive theorem proving and program development[M]. Berlin, Heidelberg: Springer, 2004.
[2]	Clarke E M, Grumberg O, Peled D. Model checking[C]// Ramesh S, Sivakumar G. Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1997. Berlin, Heidelberg: Springer, 1997: 54-56.
[3]	Myers G. The art of software testing[M]. Hoboken: John Wiley & Sons, Inc., 2004.
[4]	Leucker M, Schallhart C. A brief account of runtime verification[J]. The Journal of Logic and Algebraic Programming, 2009, 78(5): 293-303. DOI URL
[5]	Snodgrass R. A relational approach to monitoring complex systems[J]. ACM Transactions on Computer Systems, 1988, 6(2): 157-195. DOI URL
[6]	IEEE.IEEE Standard Glossary of Software Engineering Terminology:IEEE Std 610.12-1990[S]. Piscataway: IEEE Press, 1990.
[7]	Zulkernine M, Seviora R E. A compositional approach to monitoring distributed systems[C]// Proceedings of the International Conference on Dependable Systems and Networks. Piscataway: IEEE Press, 2001: 763-772.
[8]	Bauer A, Leucker M, Schallhart C. Model-based runtime analysis of distributed reactive systems[C]// Proceedings of the Australian Software Engineering Conference (ASWEC’06). Piscataway:IEEE Press, 2006: 243-252.
[9]	Gopinathan M, Rajamani S K. Runtime monitoring of object invariants with guarantee[C]// Leucker M.Proceedings of the International Workshop on Runtime Verification. Berlin, Heidelberg: Springer, 2008: 158-172.
[10]	Qu G Z, Hariri S, Jangiti S, et al. Online monitoring and analysis for self-protection against network attacks[C]// Proceedings of the International Conference on Autonomic Computing, 2004. Piscataway: IEEE Press, 2004: 324-325.
[11]	Reinbacher T, Rozier K Y, Schumann J. Temporal-logic based runtime observer Pairs for system health management of real-time systems[C]// Ábrahám E, Havelund K. Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014. Berlin, Heidelberg: Springer, 2014: 357-372.
[12]	Lattanzi E, Acquaviva A, Bogliolo A. Run-time software monitor of the power consumption of wireless network interface cards[C]// Macii E, Paliouras V, Koufopavlou O. Proceedings of the International Workshop on Power and Timing Modeling, Optimization and Simulation. Berlin, Heidelberg: Springer, 2004: 352-361.
[13]	Yu L G. Applying software wrapping on performance monitoring of web services[J]. Journal of Computer Science, 2007, 6(3): 1-6. DOI URL
[14]	Pnueli A. The temporal logic of programs[C]// Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS 1977). Piscataway:IEEE Press, 2008: 46-57.
[15]	Geilen M. On the construction of monitors for temporal logic properties[J]. Electronic Notes in Theoretical Computer Science, 2001, 55(2):181-199. DOI URL
[16]	Havelund K, Roşu G. Synthesizing monitors for safety properties[C]// Katoen J P, Stevens P.Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2002: 342-356.
[17]	Alur R, Feder T, Henzinger T A. The benefits of relaxing punctuality[J]. Journal of the ACM, 1996, 43(1): 116-146. DOI URL
[18]	Ouaknine J, Worrell J. On the decidability of metric temporal logic[C]// Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05). Piscataway:IEEE Press, 2005: 188-197.
[19]	Hirshfeld Y, Rabinovich A. Logics for real time: Decidability and complexity[J]. Fundamenta Informaticae, 2004, 62(1): 1-28.
[20]	Maler O, Nickovic D. Monitoring temporal properties of continuous signals[C]// Lakhnech Y, Yovine S.Proceedings of the International Conference on Formal Techniques, Modelling and Analysis of Timed and Fault-tolerant Systems. Berlin, Heidelberg: Springer, 2004: 152-166.
[21]	Konur S. A survey on temporal logics for specifying and verifying real-time systems[J]. Frontiers of Computer Science, 2013, 7(3): 370-403. DOI
[22]	Alur R, Henzinger T A. A really temporal logic[J]. Journal of the ACM, 1994, 41(1): 181-203. DOI URL
[23]	Ostroff J S. Temporal logic for real-time systems[M]. Taunton: Research Studies Press, 1989.
[24]	Colombo C, Pace G J, Schneider G. Dynamic event-based runtime monitoring of real-time and contextual properties[C]// Cofer D, Fantechi A. Proceedings of the International Workshop on Formal Methods for Industrial Critical Systems. Berlin, Heidelberg: Springer, 2009: 135-149.
[25]	Clarkson M R, Schneider F B. Hyperproperties[C]// Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium. Piscataway: IEEE Press, 2008: 51-65.
[26]	Clarkson M R, Finkbeiner B, Koleini M, et al. Temporal logics for hyperproperties[DB/OL]. arXiv preprint: 1401.4492, 2014.
[27]	Agrawal S, Bonakdarpour B. Runtime verification of k-safety hyperproperties in HyperLTL[C]// Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium (CSF). Piscataway:IEEE Press, 2016: 239-252.
[28]	Mok A K, Liu G T. Efficient Run-time monitoring of timing constraints[C]// Proceedings of the Third IEEE Real-time Technology and Applications Symposium. Piscataway: IEEE Press, 2002: 252-262.
[29]	Jahanian F, Rajkumar R, Raju S C V. Runtime monitoring of timing constraints in distributed real-time systems[J]. Real-time Systems, 1994, 7(3): 247-273. DOI URL
[30]	Kristoffersen K J, Pedersen C, Andersen H R. Runtime verification of timed LTL using disjunctive normalized equation systems[J]. Electronic Notes in Theoretical Computer Science, 2003, 89(2): 210-225. DOI URL
[31]	Thati P, Roşu G. Monitoring algorithms for metric temporal logic specifications[J]. Electronic Notes in Theoretical Computer Science (ENTCS), 2005, 113(C): 145-162.
[32]	Kini D R, Krishna S N, Pandya P K. On construction of safety signal automata for MITL[u, s] using temporal projections[C]// Fahrenberg U, Tripakis S. Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems. Berlin, Heidelberg: Springer, 2011: 225-239.
[33]	Geilen M, Dams D. An on-the-fly tableau construction for a real-time temporal logic[C]// Joseph M.Proceedings of the 6th International Symposium on Formal Techniques in Real-time and Fault-tolerant Systems.Berlin, Heidelberg: Springer, 2000: 276-290.
[34]	Drusinsky D. On-line monitoring of metric temporal logic with time-series constraints using alternating finite automata[J]. Journal of Universal Computer Science, 2006, 12(5): 482-498.
[35]	Basin D, Klaedtke F, Müller S, et al. Monitoring metric first-order temporal properties[J]. Journal of the ACM, 2015, 62(2): 1-45.
[36]	Basin D, Klaedtke F, Zălinescu E. Algorithms for monitoring real-time properties[J]. Acta Informatica, 2018, 55(4): 309-338. DOI URL
[37]	Simko G, Sztipanovits J. Active monitoring using real-time metric linear temporal logic specifications[C]// Conchon E, CorreiaC M B A, FredA L N, et al.Proceedings of the International Conference on Health Informatics. 2012, doi: 10.5220/0003768703700373.
[38]	Pinisetty S, Falcone Y, Jéron T, et al. Runtime enforcement of timed properties[C]// Qadeer S, Tasiran S.Proceedings of the 4th International Conference on Runtime Verification. Berlin, Heidelberg: Springer, 2013: 229-244.
[39]	Baldor K, Niu J W. Monitoring dense-time, continuous-semantics, metric temporal logic[C]// Qadeer S, Tasiran S. Proceedings of the 4th International Conference on Runtime Verification. Berlin, Heidelberg: Springer, 2013: 245-259.
[40]	de Matos Pedro A, Pereira D, Pinho L M, et al. A compositional monitoring framework for hard real-time systems[C]// Badger J M, Rozier K Y. Proceedings of the 6th NASA Formal Methods Symposium. Cham: Springer, 2014: 16-30.
[41]	Bauer A, Leucker M, Schallhart C. Monitoring of real-time properties[C]// Arum-Kumar S, Grag N.Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science. Berlin, Heidelberg: Springer, 2006: 260-272.
[42]	Arafat O, Bauer A, Leucker M, et al. Runtime verification revisited[R]. Munich: Technical University of Munich, 2005.
[43]	Bauer A, Leucker M, Schallhart C. Runtime verification for LTL and TLTL[J]. ACM Transactions on Software Engineering and Methodology, 2011, 20(4), doi: 10.1145/2000799.2000800. DOI
[44]	Bauer A, Leucker M, Schallhart C. The good, the bad, and the ugly, but how ugly is ugly?[C]// Sokolsky O, Taşiran S. Proceedings of the 7th International Workshop on Runtime Verification. Berlin, Heidelberg: Springer, 2007: 126-138.
[45]	Mitsch S, Platzer A. ModelPlex: Verified runtime validation of verified cyber-physical system models[J]. Formal Methods in System Design, 2016, 49(1-2): 33-74. DOI URL
[46]	Fraigniaud P, Rajsbaum S, Travers C. On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems[C]// Bonakdarpour B, Smolka S A. Proceedings of the 5th International Conference on Runtime Verification. Cham: Springer, 2014: 92-107.
[47]	de Matos Pedro A, Pereira D, Pinho L M, et al. Monitoring for a decidable fragment of MTL-∫[M]// BartocciE, MajumdarR. RuntimeVerification. Cham: Springer International Publishing, 2015: 169-184.
[48]	Singh N K, Saha I. Specification-guided automated debugging of CPS models[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 39(11): 4142-4153. DOI URL
[49]	Kane A, Chowdhury O, Datta A, et al. A case study on runtime monitoring of an autonomous research vehicle (ARV) system[M]// BartocciE, MajumdarR. Proceedings of the 6th Runtime Verification. Cham: Springer, 2015: 102-117.
[50]	Aiello M, Berryman J, Grohs J, et al. Run-time assurance for advanced flight-critical control systems*[C]// AIAA Guidance, Navigation, and Control Conference. Reston: AIAA, 2010, doi: 10.2514/6.2010-8041.
[51]	Luo H Y, Liu X, Liu J, et al. Runtime verification of business cloud workflow temporal conformance[J]. IEEE Transactions on Services Computing, 2022, 15(2): 833-846. DOI URL
[52]	Johnson T T, Bak S, Caccamo M, et al. Real-time reachability for verified simplex design[J]. ACM Transactions on Embedded Computing Systems, 2016, 15(2): 1-27.
[53]	Chen X, Sankaranarayanan S. Model predictive real-time monitoring of linear systems[C]// Proceedings of the 2017 IEEE Real-time Systems Symposium (RTSS). Piscataway:IEEE Press, 2018: 297-306.
[54]	Chen X, Sankaranarayanan S. Decomposed reachability analysis for nonlinear systems[C]// Proceedings of the 2016 IEEE Real-time Systems Symposium (RTSS). Piscataway:IEEE Press, 2017: 13-24.
[55]	Schneider F B. Enforceable security policies[C]// Foundations of Intrusion Tolerant Systems, 2003. Piscataway: IEEE Press, 2004: 117-137.
[56]	Falcone Y. You should better enforce than verify[C]// Barringer H, Falcone Y, Finkbeiner B, et al.Proceedings of the First International Conference on Runtime Verification. Berlin, Heidelberg: Springer, 2010: 89-105.
[57]	Ligatti J, Bauer L, Walker D. Run-time enforcement of nonsafety policies[J]. ACM Transactions on Information and System Security, 2009, 12(3): 1-41.
[58]	Lanotte R, Merro M, Munteanu A. Runtime enforcement for control system security[C]// Proceedings of the 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). Piscataway:IEEE Press, 2020: 246-261.
[59]	Lanotte R, Merro M, Munteanu A. Industrial control systems security via runtime enforcement[J]. ACM Transactions on Privacy and Security, 2023, 26(1): 1-41.
[60]	Pinisetty S, Roop P S, Smyth S, et al. Runtime enforcement of cyber-physical systems[J]. ACM Transactions on Embedded Computing Systems, 2017, 16(5s): 1-25.
[61]	Hu C, Dong D, Yang Y, et al. Decentralized runtime enforcement for robotic swarms[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(11): 1591-1606.
[62]	Blanco J L, Fernandez-Madrigal J A, Gonzalez J. Efficient probabilistic range-only SLAM[C]// Proceedings of the 2008 IEEE/RSJ International Conference on Intelligent Robots and Systems. Piscataway: IEEE Press, 2008: 1017-1022.
[63]	Barth A, Franke U. Where will the oncoming vehicle be the next second?[C]// Proceedings of the 2008 IEEE Intelligent Vehicles Symposium. Piscataway: IEEE Press, 2008: 1068-1073.
[64]	Houenou A, Bonnifait P, Cherfaoui V, et al. Vehicle trajectory prediction based on motion model and maneuver recognition[C]// Proceedings of the 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems. Piscataway: IEEE Press, 2014: 4363-4369.
[65]	刘志强, 吴雪刚, 倪捷, 等. 基于HMM和SVM级联算法的驾驶意图识别[J]. 汽车工程, 2018, 40(7): 858-864.
[66]	李建平. 面向智能驾驶的交通车辆运动预测方法研究[D]. 长春: 吉林大学, 2018.
[67]	Hubmann C, Quetschlich N, Schulz J, et al. A POMDP maneuver planner for occlusions in urban scenarios[C]// Proceedings of the 2019 IEEE Intelligent Vehicles Symposium (IV). Piscataway:IEEE Press, 2019: 2172-2179.
[68]	Sun K, Schlotfeldt B, Pappas G J, et al. Stochastic motion planning under partial observability for mobile robots with continuous range measurements[J]. IEEE Transactions on Robotics, 2021, 37(3): 979-995. DOI URL
[69]	Blackmore L, Ono M, Williams B C. Chance-constrained optimal path planning with obstacles[J]. IEEE Transactions on Robotics, 2011, 27(6): 1080-1094. DOI URL
[70]	Zhu H, Alonso-Mora J. Chance-constrained collision avoidance for MAVs in dynamic environments[J]. IEEE Robotics and Automation Letters, 2019, 4(2): 776-783. DOI
[71]	da Silva Arantes M, Toledo C F M, Williams B C, et al. Collision-free encoding for chance-constrained nonconvex path planning[J]. IEEE Transactions on Robotics, 2019, 35(2): 433-448. DOI URL
[72]	Henzinger T A. The theory of hybrid automata[C]// Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. Piscataway: IEEE Press, 2002: 278-292.
[73]	Branicky M S, Borkar V S, Mitter S K. A unified framework for hybrid control: Model and optimal control theory[J]. IEEE Transactions on Automatic Control, 1998, 43(1): 31-45. DOI URL
[74]	Xu X P, Antsaklis P J. Results and perspectives on computational methods for optimal control of switched systems[C]// Maler O, Pnueli A.Proceedings of the 6th International Workshop on Hybrid Systems:Computation and Control. Berlin, Heidelberg: Springer, 2003: 540-555.
[75]	Egerstedt M, Wardi Y, Axelsson H. Transition-time optimization for switched-mode dynamical systems[J]. IEEE Transactions on Automatic Control, 2006, 51(1): 110-115. DOI URL
[76]	Caldwell T M, Murphey T D. An adjoint method for second-order switching time optimization[C]// Proceedings of the 49th IEEE Conference on Decision and Control (CDC). Piscataway:IEEE Press, 2011: 2155-2162.
[77]	Johnson E R, Murphey T D. Second-order switching time optimization for nonlinear time-varying dynamic systems[J]. IEEE Transactions on Automatic Control, 2011, 56(8): 1953-1957. DOI URL
[78]	Gonzalez H, Vasudevan R, Kamgarpour M, et al. A descent algorithm for the optimal control of constrained nonlinear switched dynamical systems[C]// Proceedings of the 13th ACM international conference on Hybrid systems:Computation and control. New York: ACM Press, 2010: 51-60.
[79]	Ali U, Egerstedt M. Hybrid optimal control under mode switching constraints with applications to pesticide scheduling[J]. ACM Transactions on Cyber-Physical Systems, 2018, 2(1): 1-17.
[80]	Nilsson P, Ozay N. Incremental synthesis of switching protocols via abstraction refinement[C]// Proceedings of the 53rd IEEE Conference on Decision and Control. Piscataway: IEEE Press, 2015: 6246-6253.
[81]	Ding X C, Wardi Y, Egerstedt M. On-line optimization of switched-mode dynamical systems[J]. IEEE Transactions on Automatic Control, 2009, 54(9): 2266-2271. DOI URL
[82]	Branicky M S, Curtiss M M, Levine J A, et al. RRTs for nonlinear, discrete, and hybrid planning and control[C]// Proceedings of the 42nd IEEE International Conference on Decision and Control (IEEE Cat. No.03CH37475). Piscataway:IEEE Press, 2004: 657-663.
[83]	Farahani S S, Raman V, Murray R M. Robust model predictive control for signal temporal logic synthesis[J]. IFAC-PapersOnLine, 2015, 48(27): 323-328. DOI URL
[84]	Sha L. Using simplicity to control complexity[J]. IEEE Software, 2001, 18(4): 20-28.
[85]	Pek C, Manzinger S, Koschi M, et al. Using online verification to prevent autonomous vehicles from causing accidents[J]. Nature Machine Intelligence, 2020, 2(9): 518-528. DOI
[86]	Zhao C Z, Dong W, Qi Z C. Active monitoring for control systems under anticipatory semantics[C]// Proceedings of the 2010 10th International Conference on Quality Software. Piscataway: IEEE Press, 2010: 318-325.
[87]	Yu K, Chen Z B, Dong W. A predictive runtime verification framework for cyber-physical systems[C]// Proceedings of the 2014 IEEE Eighth International Conference on Software Security and Reliability-Companion. Piscataway: IEEE Press, 2014: 223-227.
[88]	Chen Z, Wang C, Yan J Q, et al. Runtime detection of memory errors with smart status[C]// Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York: ACM Press, 2021: 296-308.
[89]	Chen Z, Yan J Q, Kan S L, et al. Detecting memory errors at runtime with source-level instrumentation[C]// Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York: ACM Press, 2019: 341-351.
[90]	Chen Z, Zhang Q, Wu J, et al. A source-level instrumentation framework for the dynamic analysis of memory safety[J]. IEEE Transactions on Software Engineering, 2022, doi: 10.1109/TSE.2022.3210580. DOI
[91]	Chen Z, Wu J, Zhang Q, et al. A dynamic analysis tool for memory safety based on smart status and source-level instrumentation[C]// Proceedings of the 2022 IEEE/ACM 44th International Conference on Software Engineering:Companion Proceedings (ICSE-Companion). Piscataway:IEEE Press, 2022: 6-10.
[92]	Chen Z, Wang Z M, Zhu Y L, et al. Parametric runtime verification of C programs[C]// Chechik M, Raskin J F. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2016: 299-315.
[93]	Chen Z. Parametric runtime verification is NP-complete and coNP-complete[J]. Information Processing Letters, 2017, 123: 14-20. DOI URL
[94]	Chen Z, Chen Y Y, Hierons R M, et al. Four-valued monitorability of ω-regular languages[C]// Lin S W, Hou Z, Mahony B. Proceedings of the 22nd International Conference on Formal Methods and Software Engineering. Cham: Springer, 2020: 198-214.
[95]	Bu L, Wang Q X, Ren X Y, et al. Scenario-based online reachability validation for CPS fault prediction[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 39(10): 2081-2094. DOI URL
[96]	Wang J W, Bu L, Xing S P, et al. PDF: Path-oriented, derivative-free approach for safety falsification of nonlinear and nondeterministic CPS[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022, 41(2): 238-251 DOI URL
[97]	Xing S P, Wang J W, Bu L, et al. Approximate optimal hybrid control synthesis by classification-based derivative-free optimization[C]// Proceedings of the 24th International Conference on Hybrid Systems:Computation and Control. New York: ACM Press, 2021: 10.1145/3447928.3456658.
[98]	Wang J W, Bu L, Xing S P, et al. Combined online checking and control synthesis: A study on a vehicle platoon testbed[C]// Huisman M, Pǎsǎreanu C, Zhan N. Proceedings of the 24th International Symposium on Formal Methods. Cham: Springer, 2021: 752-762.
[99]	Xue B, Zhan N J, Fränzle M, et al. Reach-avoid verification based on convex optimization[DB/OL]. arXiv preprint: 2208.08105, 2022.
[100]	Xue B, Li R J, Zhan N J, et al. Reach-avoid analysis for stochastic discrete-time systems[C]// Proceedings of the 2021 American Control Conference (ACC). Piscataway:IEEE Press, 2021: 4879-4885.
[101]	Xue B, Fränzle M, Zhan N J. Inner-approximating reachable sets for polynomial systems with time-varying uncertainties[J]. IEEE Transactions on Automatic Control, 2020, 65(4): 1468-1483. DOI URL
[102]	Huang K, Santinelli L, Chen J J, et al. Adaptive dynamic power management for hard real-time systems[C]// Proceedings of the 2009 30th IEEE Real-time Systems Symposium. Piscataway: IEEE Press, 2009: 23-32.
[103]	Yan R, Zhu D, Zhang F, et al. Resource-aware design for reliable autonomous applications with multiple periods[C]// Havelund K, Peleska J, Roscoe B, et al. Proceedings of the 22nd International Symposium on Formal Methods. Cham: Springer, 2018: 294-311.
[104]	Hu B, Huang K, Chen G, et al. Adaptive workload management in mixed-criticality systems[J]. ACM Transactions on Embedded Computing Systems, 2017, 16(1): 1-27.
[105]	Huang K, Chen G, Buckl C, et al. Conforming the runtime inputs for hard real-time embedded systems[C]// Proceedings of the 49th Annual Design Automation Conference. New York: ACM Press, 2012: 430-436.
[106]	Hu B, Huang K, Chen G, et al. Adaptive runtime shaping for mixed-criticality systems[C]// Proceedings of the 2015 International Conference on Embedded Software (EMSOFT). Piscataway:IEEE Press, 2015: 11-20.
[107]	单云霄, 黄润辉, 何泽, 等. 深度纯追随的拟人化无人驾驶转向控制模型[J]. 中国图象图形学报, 2021, 26(1): 176-185.
[108]	Shan Y X, Zheng B L, Chen L S, et al. A reinforcement learning-based adaptive path tracking approach for autonomous driving[J]. IEEE Transactions on Vehicular Technology, 2020, 69(10): 10581-10595. DOI URL
[109]	Shan Y X, Yao X T, Lin H Q, et al. Lidar-based stable navigable region detection for unmanned surface vehicles[J]. IEEE Transactions on Instrumentation and Measurement, 2021, 70: 1-13.
[110]	Shan Y X, Zhou X M, Liu S H, et al. SiamFPN: A deep learning method for accurate and real-time maritime ship tracking[J]. IEEE Transactions on Circuits and Systems for Video Technology, 2021, 31(1): 315-325. DOI URL

特性	详细描述
可观察性（Observation-based）	监控器应该重点考虑原系统控制器的可观察性，而不查看在其内部（可能是模糊的）执行代码
确定性（Determinism Preservation）	RE中的防护器生成算法不应该引入非确定性
可用性（Feasibility）	防护器生成算法的复杂度应该是多项式的
避免死锁（Deadlock-freedom）	强制过程不能在被监控系统中引入死锁
避免分歧（Divergence-freedom）	强制过程不能在被监控系统中引入分歧
可扩展性（Scalability）	算法应该具备足够的可扩展性以适应原系统控制器

特性	详细描述
可观察性（Observation-based）	监控器应该重点考虑原系统控制器的可观察性，而不查看在其内部（可能是模糊的）执行代码
确定性（Determinism Preservation）	RE中的防护器生成算法不应该引入非确定性
可用性（Feasibility）	防护器生成算法的复杂度应该是多项式的
避免死锁（Deadlock-freedom）	强制过程不能在被监控系统中引入死锁
避免分歧（Divergence-freedom）	强制过程不能在被监控系统中引入分歧
可扩展性（Scalability）	算法应该具备足够的可扩展性以适应原系统控制器

Current Status and Prospects of Runtime Software Verification and Monitoring

软件运行时验证与监控技术发展现状与展望

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 2

References 110

Related Articles 0

Recommended Articles

Metrics

Access Statistics

Links

Contact Us

WeChat