一种基于预测的运行时验证开销控制方法

doi:10.3969/j.issn.1006-2475.2016.04.019

摘要/Abstract

摘要： 针对运行时验证中，监控模块对软件系统运行效率产生影响的问题，提出一种基于预测的控制运行时验证开销的方法。该方法主要是通过建立马尔可夫链（Markov Chain）和隐马尔可夫模型（Hidden Markov Model, HMM）对软件行为进行有限步的预测，并判断被验证的性质约束被违反的风险，依此对软件监控行为进行调整，从而实现将运行时验证所产生的额外开销控制在一定范围内的目标。这种方法能够有效地控制监控开销，但仍然需要进一步的研究。

关键词: 运行时验证, 马尔科夫链, 隐马尔可夫模型, 软件行为预测, 开销控制

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

中图分类号:

TP311

胡磊，江国华. 一种基于预测的运行时验证开销控制方法[J]. 计算机与现代化, doi: 10.3969/j.issn.1006-2475.2016.04.019.

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.

参考文献

［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]	祝丁恺, 铁治欣, 洪顺贺. 一种HRG模型初始化算法及在链路预测中的应用[J]. 计算机与现代化, 2022, 0(02): 38-44.
[2]	许国艳1,朱进1,司存友2,胡文斌2,刘凡1. 基于CNN和MC的水文时间序列预测组合模型[J]. 计算机与现代化, 2019, 0(11): 23-.
[3]	熊苏生１,2. 基于改进LightGBM的交通模式识别算法[J]. 计算机与现代化, 2018, 0(10): 68-.
[4]	刘德春1，张秀国2，姜微2. 基于马尔科夫链的大学生自主学习能力预测方法[J]. 计算机与现代化, 2018, 0(05): 106-.
[5]	朱春媚1，2，黎萍1. 基于支持向量机的咳嗽自动识别[J]. 计算机与现代化, 2016, 251(07): 111-114.
[6]	任晓娜1，裴祥2. 基于线性网络编码的无线网络信道接入机制[J]. 计算机与现代化, 2015, 0(6): 92-96.
[7]	马银雪，李文明，陈哲. 基于对象的C程序边界安全检测改进技术[J]. 计算机与现代化, 2015, 0(10): 25-30.
[8]	黄志成. 隐马尔可夫模型在学习系统信息挖掘中的应用[J]. 计算机与现代化, 2013, 1(6): 13-15.
[9]	史倩. 基于LSA-HMM的新闻主题分割[J]. 计算机与现代化, 2012, 1(201): 27-30,3.
[10]	李战明;宋丙菊. 改进Hu矩的ATM机异常行为识别研究[J]. 计算机与现代化, 2012, 1(200): 188-04.
[11]	许帅;隋平. 一种基于MaC的运行时验证框架的研究[J]. 计算机与现代化, 2010, 1(01): 188-190.