参数化运行时监控研究

doi:10.11896/j.issn.1002-137X.2014.11.029

摘要/Abstract

摘要： 随着计算机软件广泛应用于各类安全关键系统以及软件日趋复杂,软件可靠性变得越来越重要。作为一种广泛使用于各种平台的软件解决方案,运行时监控是提高软件可靠性的最灵活的解决方案之一。但随着运行时监控技术以及软件技术的发展,人们希望通过运行时监控技术来验证系统的动态属性,从而提出参数化性质的运行时监控技术。由于其在面向对象系统中的适用性,参数化性质的运行时监控已经受到了越来越多的关注。综述了参数化运行时监控的研究进展,提出了参数化运行时监控的问题定义,介绍了这一领域的主要研究内容:参数化运行时监控方法、减少参数化监控开销的技术、多属性规约的参数化运行时监控。

关键词: 运行时监控,参数化性质规约,参数化运行时监控

Abstract: With the wide application of software in all kinds of safety critical systems as well as the increasingly complexity,software reliability becomes more and more important.As a software solution widely used in various platforms,runtime monitoring is one of the most flexible solution to enhance the reliability of software.With the development of runtime monitoring and software technology,people want to verify the dynamic properties of system through runtime monitoring.So runtime monitoring of parametric properties was presented.Runtime monitoring of parametric properties have achieved more and more attention because of its applicability in the object-oriented system.This paper summarized the researches on parametric runtime verification,presented the problem definition of parametric runtime verification,and introduced the main research content of this field,including parametric runtime verification approaches,technologies of reducing parametric monitoring overhead and runtime monitoring of multiply parametric properties.

Key words: Runtime monitoring,Parametric property specification,Parametric runtime monitoring

王珍,叶俊民,陈曙,辜剑,金聪. 参数化运行时监控研究[J]. 计算机科学, 2014, 41(11): 146-151. https://doi.org/10.11896/j.issn.1002-137X.2014.11.029

WANG Zhen,YE Jun-min,CHEN Shu,GU Jian and JIN Cong. Research on Parameterized Runtime Monitoring[J]. Computer Science, 2014, 41(11): 146-151. https://doi.org/10.11896/j.issn.1002-137X.2014.11.029

参考文献

[1] Clarke E M,Wing J M.Formal methods:State of the art and future directions[J].ACM Computing Surveys,1996,28(4):626-643
[2] Clarke E M,Grumberg O,Peled D A.Model Checking[M].Massachusetts:The MIT Press,1999
[3] Gabbay D M,Hogger C J,Robinson J A,et al.Handbook of Logic in artificial Intelligence and Logic Programming[C]∥Vo-lume2,Deduction Methodologies.London:Oxford University Press,1994
[4] Blum M,Kannan S.Designing programs that check their work[J].Journal of the ACM,1995,42(1):269-291
[5] Bauer A,Leucker M,Schallhart C.Runtime Verification forLTL and TLTL[J].ACM Transactions on Software Enginee-ring and Methodology,2011,20(4):1-64
[6] Havelund K,Rosu G.Synthesizing Monitors for Safety Properties[C]∥Proceedings of the 8^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.London,UK,2002:342-356
[7] Bodden E,Hendren L,Lam P,et al.Collaborative runtime verification with tracematches[C]∥Proceedings of the 7^th international conference on Runtime Verification.Berlin,Germany,2007:22-37
[8] Bodden E.A lightweight LTL runtime verification tool for Java[C]∥Proceedings of the 9^th Annual ACM SIGPLAN Confe-rence on Object-oriented Programming,Systems,Languages,and Applications.New York,USA,2004:306-307
[9] Havelund K,Rosu G.Monitoring Java Program with JavaPath Explorer[J].Electronic Notes in Theoretical Computer Science,2001,55(2):200-217
[10] Kim M,Kannan S,Lee L,et al.Java-MaC:a run-time assurance approach for Java programs[J].Formal Methods in System Design,2004,24(2):129-155
[11] 赵常智,董威,隋平,等.面向参数化LTL的预测监控器构造技术[J].软件学报,2010,21(2):318-333
[12] Bodden E.J-LO-A tool for runtime-checking temporal assertions[D].Germany:RWTH Aachen University,2005
[13] Avgustinov P,Tibblw J,de Moor O.Making Trace Monitors Feasible[C]∥Proceedings of the 22^nd Annual ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications.New York,USA,2007:589-608
[14] Alan C,Avgustinov P,Christensen A S,et al.Adding tracematching with free variables to AspectJ[C]∥Proceedings of the 20^th Annual ACM SIGPLAN Conference on Object-oriented Programming,Systems,Languages,and Applications.New York,USA,2005:345-364 (下转第174页)(上接第151页)
[15] Martin M,Livshits B,Lam M S.Finding Application Errors and Security Flaws Using PQL:a Program Query Language[C]∥Proceedings of the 20^th annual ACM SIGPLAN conference on Object-oriented programming,systems,languages,and applications.New York,USA,2005:365-383
[16] Goldsmith S,O’Callahan R,Aiken A.Relational Queries Over Program Traces[C]∥Proceedings of the 20^th Annual ACM SIGPLAN Conference on Object-oriented Programming,Systems,Languages,And Applications.New York,USA,2005:385-402
[17] Barringer H,Goldberg A,Havelund K,et al.Rule-Based Runtime Verification[C]∥Proceedings of the 5^th International Conference on Verification,Model Checking,and Interpretation(VMCAI 2004).Venice,Italy,2004:44-57
[18] Barringer H,Rydeheard D,Havelund K.Rule systems for runtime monitoring:from EAGLE to RULER[C]∥Proceedings of the 7^th International Workshop on Runtime Verification.Vancover,Canada,2007:111-125
[19] Dwyer M B,Purandare R.Residual dynamic typestate analysis exploiting static analysis:results to reformulate and reduce the cost of dynamic analysis[C]∥Proceedings of the 22^nd IEEE/ACM International Conference on Automated Software Engineering.New York,USA,2007:124-133
[20] Bodden E,Hendren L,Lhotak O.A staged static program analysis to improve the performance of runtime monitoring[C]∥Proceedings of the 21^st European conference on Object-Oriented Programming.Berlin,Germany,2007:525-549
[21] Bodden E,Feng Chen,Rosu G.Dependent Advice:A GeneralApproach to Optimizing History-based Aspects[C]∥Procee-dings of the 8^th International Conference on Aspect-Oriented Software Development.Virginia,USA,2009:3-14
[22] Bodden E,Lam P,Hendren L.Clara:a Framework for Partially Evaluating Finite-state Runtime Monitors Ahead of Time[C]∥Proceedings of the First International Conference on Runtime Verification.Julians,Malta,2010:183-197
[23] Chen Feng,Jin Dong-yun,Meredith P O,et al.Efficient Forma-lism-Independent Monitoring of Parametric Properties[C]∥Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering.Washington,USA,2009:383-394
[24] Jin Dong-yun,Meredith P O,Lee C,et al.JavaMOP:efficient parametric runtime monitoring framework[C]∥Proceedings of the 2012 International Conference on Software Engineering.Piscataway,USA,2012:1427-1430
[25] Chen Feng,Rosu G.MOP:An Efficient and Generic RuntimeVerification Framework[C]∥Proceedings of the 22^nd annual ACM SIGPLAN conference on Object-oriented programming,systems,languages,and applications.New York,USA,2007:569-588
[26] Jin Dong-yun.Making Runtime Monitoring of Parametric Properties Practical[D].USA:University of Illinois at Urbana-Champaign,2012
[27] Jin Dong-yun,Meredith P O,Griffith D,et al.Garbage Collection for Monitoring Parametric Properties[C]∥Proceedings of the 32^nd ACM SIGPLAN Conference on Programming Language Design and Implementation.New York,USA,2011:415-424
[28] Avgustinov P,Tibble J,Bodden E,et al.Efficient Trace Monitoring[C]∥Proceedings of the 21^st ACM SIGPLAN Symposium on Object-oriented Programming Systems,Languages,and Applications.New York,USA,2006:685-686
[29] Meredith P O,Jin Dong-yun,Chen Feng,et al.Efficient Monitoring of Parametric Context-Free Patterns[J].Automated Software Engineering,2010,17(2):149-180
[30] Rosu G,Chen Feng.Semantics and Algorithms for ParametricMonitoring[J].Logical Methods in Computer Science,2012,8(1):1-47
[31] Chen Feng,Rosu G.Parametric Trace Slicing and Monitoring[C]∥Proceeding of the 15^th International Conference on Tools and Algorithms for the Construction and Analysis of the Systems.Berlin,Germany,2009:246-261

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed