A Control Method of Runtime Verification Overhead Based on Prediction

doi:10.3969/j.issn.1006-2475.2016.04.019

Abstract

Abstract:

For the problem that monitoring module affects the operating efficiency of the software system when runtime verifying, a method of control runtime verification overhead based on prediction was proposed. Chain Markov and Hidden Markov Model (HMM) were used to predict the behavior of the software, and the risk of the constraint being violated would be controlled. According to this, the monitoring behavior of the software was adjusted to achieve the goal of extra overhead produced in runtime verifying being controlled in some ranges. This method can control the cost of monitoring effectively, but still needs improvement.

Key words:

text-indent: 21pt">runtime verification, Markov chain, hidden Markov model, prediction of software behavior, overhead control

CLC Number:

TP311

HU Lei， JIANG Guo-hua.

A Control Method of Runtime Verification Overhead Based on Prediction[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2016.04.019.

References

［1］ Colin S, Mariani L. Run-time verification［C］// Model-Based Testing of Reactive System. LNCS:3472. 2005:525-555.

［2］ Whittaker J A. What is software testing? and why is it so hard?［J］. IEEE Software, 2000,17(1):70-79.

［3］ Bérard B, Bidoit M, Finkel A, et al. Systems and Software Verification: ModelChecking Techniques and Tools［M］. Springer Berlin Heidelberg, 2001.

［4］赵常智. 基于运行时验证的软件监控关键技术研究［D］. 长沙:国防科学技术大学, 2011.

［5］ Maggi F M, Westergaard M, Montali M, et al. Runtime verification of LTL-based declarative process models［C］// The 2rd International Conference on Runtime Verification. 2012,7186:131-146.

［6］ Becchi M, Crowley P. Efficientregular expression evaluation: Theory to practice［C］// Proceedings of the 4th ACM/IEEE Symposium on Architectures for Networking and Communications Systems. 2008:50-59.

［7］ Bhorkar A. A run-time assertion checker for Java using JML［R］. Iowa State University: Computer Science Technical Reports, 2000.

［8］ Li X, Qiu X, Wang L, et al. UML interaction modeldriven runtime verification of Java programs［J］. IET software, 2011,5(2):142-156.

［9］邵津,邓芳,王千祥. 一种基于模型的软件系统监测方法［J］. 计算机研究与发展, 2010,47(7):1175-1183.

［10］Clavel M, Durán F, Eker S, et al. Maude: Specification and programming in rewriting logic［J］. Theoretical Computer Science, 2001,285(2):187-243.

［11］Mok A K, Liu Guangtian. Efficient run-time monitoring of timing constraints［C］// Proceedings of the 3rd IEEE Real-Time Technology and Applications Symposium. 1997:252-262.
［12］Stolz V, Bodden E. Temporal assertions using aspectJ［J］. Electronic Notes in Theoretical Computer Science, 2006,144(4):109-124.

［13］Gastin P, Oddoux D. Fast LTL to Büchi Automata Translation［M］// Computer Aided Verification:Proceedings of the 13th International Conference on CAV. 2001, 2102:53-65.

［14］Bodden E, Hendren L, Lhoták O. A staged static program analysis to improve the performance of runtime monitoring［C］// Proceedings of the 21st European Conference on Object-Oriented Programming. 2007:525-549.

［15］张剑. 多核处理器架构下软件运行时验证方法研究［D］. 南京:南京航空航天大学, 2010.

［16］Berkovich S, Bonakdarpour B, Fischmeister S. GPU-based runtime verification［C］// 2013 IEEE 27th International Symposium on Parallel & Distributed Processing (IPDPS). 2013:1025-1036.

［17］d’Amorim M, Havelund K. Event-based runtime verification of Java programs［J］. ACM SIGSOFT Software Engineering Notes, 2005,30(4):1-7.

［18］Bonakdarpour B, Navabpour S, Fischmeister S. Path-aware time-triggered runtime verification［J］. Formal Methods in System Design, 2013,43(1):29-60.

［19］王珍. 实时系统的运行时验证研究［D］. 武汉：华中师范大学, 2014.

［20］李业华,顾乃杰,张颖楠,等. 基于插桩和布尔逻辑的运行时程序验证框架［J］. 计算机工程, 2013,39(1):29-34.

［21］Martin L Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming［M］. Wiley-Interscience, 1994.

［22］Eddy S R. Profile hidden Markov models［J］. Bioinformatics, 1998,14(9):755-763.

［23］张胜娜. 含有隐变量的高阶马尔科夫模型的理论及应用［D］. 成都:电子科技大学, 2014.

［24］杜世平. 隐马尔可夫模型的原理及其应用［D］. 成都:四川大学, 2004.

［25］Kim M Z, Viswanathan M, Kannan S, et al. Java-MaC: A run-time assurance approach for Java programs［J］. Formal Methods in System Design, 2004,24(2):129-155.

[1]	ZHU Ding-kai, TIE Zhi-xin, HONG Shun-he. An Initialization Algorithm of HRG Model and Its Application in Link Prediction [J]. Computer and Modernization, 2022, 0(02): 38-44.
[2]	CUI Wen-di, DUAN Peng-fei, ZHU Hong-qiang, LIU Na. Security Risk Assessmenton of Attack Graph and HMM Industrial Control Network [J]. Computer and Modernization, 2020, 0(07): 32-37.
[3]	XU Guo-yan1, ZHU Jin1, SI Cun-you2, HU Wen-bin2, LIU Fan1. Combined Hydrological Time Series Forecasting Model Based on CNN and MC [J]. Computer and Modernization, 2019, 0(11): 23-.
[4]	XIONG Su-sheng1，2. Identifying Transportation Mode Based on Improved LightGBM Algorithm [J]. Computer and Modernization, 2018, 0(10): 68-.
[5]	LIU De-chun1, ZHANG Xiu-guo2, JIANG Wei2. Self-regulated Learning Ability Prediction for College Students Based on Markov Chain [J]. Computer and Modernization, 2018, 0(05): 106-.
[6]	JU Xing-kong. Simulation of Web Crawler Detection Algorithm Based on Hidden Markov Model [J]. Computer and Modernization, 2017, 0(4): 122-126.
[7]	LI Jin-hua1, ZHEN Hui2, HUANG Hai1, YAO Jian3. Android Client for Dynamic ECG Monitoring System Based on BLE [J]. Computer and Modernization, 2016, 0(4): 114-122.
[8]	WANG Xiao-xi1, WU Gang1, WANG Hao2. Architecture Design and Business Implementation of High Concurrency High Availability Retail O2O Trade System [J]. Computer and Modernization, 2016, 0(4): 100-108.
[9]	JI Zhong-xiao, JIANG Guo-hua. A Positioning Method of Safety Critical Function Based on FTA and FDG [J]. Computer and Modernization, 2016, 0(4): 85-89+122.
[10]	ZHU Ya-hui, CHEN Dan, ZHUANG Yi. Virtual Machine Scheduling Algorithm Based on Energy-Aware in Cloud Data Center [J]. Computer and Modernization, 2016, 0(4): 74-78.
[11]	CAI Yi-qing, ZHANG Ya, ZHANG Song. Design of Magazine Counter Based on MSP430F149 [J]. Computer and Modernization, 2016, 0(4): 50-53.
[12]	ZHAI Shi-wei1， SHEN Shi-gen2,3， CAO Qi-ying1. Wireless Mesh Networks Admission Control Based on Non-Cooperative Game [J]. Computer and Modernization, 2016, 0(4): 45-49+78.
[13]	CHEN Shu，WANG Ming-jia. An Equally Distributed Cluster Heads Algorithm Based on Fuzzy Logic [J]. Computer and Modernization, 2016, 0(4): 40-44+58.
[14]	LIU Zhi-peng1, YUAN Min2. An Improved Indoor Positioning Method Based on WiFi Fingerprinting [J]. Computer and Modernization, 2016, 0(4): 36-39.
[15]	MA Ming-yang. SMS Encryption Scheme for Smartphones Based on Trusted Hardware [J]. Computer and Modernization, 2016, 0(4): 29-35.