运行时验证技术的研究进展

摘要/Abstract

摘要： 运行时验证是一种轻量级的验证方法,通过实时地监测系统的行为, 验证系统的正确性,及时发现冲突,并发出警告或作出反应。运行时验证技术已经得到了越来越多的应用,以确保软件系统的正确性。总结了近年来运行时验证技术的研究进展,首先介绍了运行时验证的概念、原理和分类,接着深入分析了现有的几种解决方案,并对该领域中的研究热点进行了深入探讨,最后分析了运行时验证技术面临的主要挑战,并对未来该领域的研究方向进行了展望。

关键词: 运行时验证,运行时监控,软件正确性,形式化方法

Abstract: Runtime verification is a lightweight verification technique which monitors the behaviors of the target systems and checks whether their behaviors satisfy the desired properties.Once a violation is observed,the monitor informs the system to react in time.Runtime verification has been applied to various areas to ensure the correctness of systems.In this paper,the concepts,principles and categories of runtime verification were first introduced.Then several solutions and research hotspots in this area were analyzed.Finally,we discussed the current challenges,and outlined the future research directions of runtime verification.

Key words: Runtime verification,Runtime monitoring,Correctness of software,Formal methods

张硕,贺飞. 运行时验证技术的研究进展[J]. 计算机科学, 2014, 41(Z11): 359-363. https://doi.org/

ZHANG Shuo and HE Fei. Research Advances in Runtime Verification[J]. Computer Science, 2014, 41(Z11): 359-363. https://doi.org/

参考文献

[1] Bertot Y,Castéran P.Interactive theorem proving and program development:Coq’Art:the calculus of inductive constructions[M].Springer,2004
[2] Clarke E M,Grumberg O,Peled D A.Model checking[M].MIT press,1999
[3] Myers G J,Sandler C,Badgett T.The art of software testing[M].John Wiley & Sons,2011
[4] Leucker M,Schallhart C.A brief account of runtime verification[J].Journal of Logic and Algebraic Programming,2009,78(5):293-303
[5] 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
[6] Bodden E.MOPBox:a library approach to runtime verification[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:365-369
[7] Havelund K,Ro u G.Monitoring java programs with javapathexplorer[J].Electronic Notes in Theoretical Computer Science,2001,55(2):200-217
[8] Kim M,Kannan S,Lee I,et al.Java-MaC:a run-time assurance tool for Java programs[J].Electronic Notes in Theoretical Computer Science,2001,55(2):218-235
[9] 张献,董威,齐治昌.基于AOP的运行时验证中的冲突检测[J].软件学报,2011,22(6):1224-1235
[10] Malik S.Runtime verification:a computer architecture perspective[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:49-62
[11] Beaucamps P,Gnaedig I,Marion J Y.Behavior abstraction inmalware analysis[C]∥Runtime Verification.Springer Berlin Heidelberg,2010:168-182
[12] Milea N A,Khoo S C,Lo D,et al.Nort:Runtime anomaly-based monitoring of malicious behavior for windows[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:115-130
[13] Bucur D.Temporal Monitors for TinyOS[C]∥Runtime Verification.Springer Berlin Heidelberg,2013:96-109
[14] Basu A,Bensalem S,Bozga M,et al.Verification of an AFDX Infrastructure using Simulations and Probabilities[C]∥Runtime Verification.Springer Berlin Heidelberg,2010:330-344
[15] 张林,唐涛,徐田华,等.运行时验证及其在列车运行控制中的应用[J].铁道学报,2011,33(12):65-71
[16] Sistla A P,Clarke E M.The complexity of propositional linear temporal logics[J].Journal of the ACM(JACM),1985,32(3):733-749
[17] Leucker M.Teaching runtime verification[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:34-48
[18] Bartetzko D,Fischer C,Mller M,et al.Jass—Java with assertions[J].Electronic Notes in Theoretical Computer Science,2001,55(2):103-117
[19] Leavens G T,Cheon Y.Design by Contract with JML.http://www.bowdoin.edu/~allen/courses/cs260/readings/leavens.pdf
[20] Chen F,Ro s′ u G.Java-MOP:A monitoring oriented programming environment for Java[C]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2005:546-550
[21] Avgustinov P,Christensen A S,Hendren L,et al.abc:An extensible AspectJ compiler[C]∥Transactions on Aspect-Oriented Software Development I.Springer Berlin Heidelberg,2006:293-334
[22] Kim M,Kannan S,Lee I,et al.Java-MaC:a run-time assurance tool for Java programs[J].Electronic Notes in Theoretical Computer Science,2001,55(2):218-235
[23] Irwin J,Kickzales G,Lamping J,et al.Aspect-oriented programming[C]∥Proceedings of ECOOP.IEEE,Finland,1997:220-242
[24] Havelund K,Ro s′ u G.Monitoring java programs with javapathexplorer[J].Electronic Notes in Theoretical Computer Science,2001,55(2):200-217
[25] Barringer H,Groce A,Havelund K,et al.An entry point for formal methods:Specification and analysis of event logs[J].arXiv preprint arXiv:1003.1682,2010
[26] Avgustinov P,Tibble J,Bodden E,et al.Efficient trace monitoring[C]∥Companion to the 21st ACM SIGPLAN Symposium on Object-oriented Programming Systems,Languages,and Applications.ACM,2006:685-686
[27] Barringer H,Havelund K.TraceContract:A Scala DSL for trace analysis[M].Springer Berlin Heidelberg,2011
[28] Barringer H,Goldberg A,Havelund K,et al.Rule-based runtime verification[C]∥Verification,Model Checking,and Interpretation.Springer Berlin Heidelberg,2004:44-57
[29] Barringer H,Rydeheard D,Havelund K.Rule systems for run-time monitoring:from Eagle to RuleR[J].Journal of Logic and Computation,2010,20(3):675-706
[30] d’Angelo B,Sankaranarayanan S,Sanchez C,et al.Lola:Runtime monitoring of synchronous systems[C]∥12th International Symposium on Temporal Representation and Reasoning,2005(TIME 2005).IEEE,2005:166-174
[31] Colombo C,Pace G J,Schneider G.Larva -safer monitoring of real-time java programs(tool paper)[C]∥2009 Seventh IEEE International Conference on Software Engineering and Formal Methods.IEEE,2009:33-37
[32] d’Amorim M,Havelund K.Event-based runtime verification of Java programs[J].ACM SIGSOFT Software Engineering Notes,2005,30(4):1-7
[33] Stolz V,Bodden E.Temporal assertions using AspectJ[J].Electronic Notes in Theoretical Computer Science,2006,144(4):109-124
[34] Drusinsky D.The temporal rover and the ATG rover[M]∥SPIN Model Checking and Software Verification.Springer Berlin Heidelberg,2000:323-330
[35] Aktug I,Naliuka K.ConSpec-a formal language for policy specification[J].Electronic Notes in Theoretical Computer Science,2008,197(1):45-58
[36] Bodden E.MOPBox:a library approach to runtime verification[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:365-369
[37] Havelund K, Ro s′ u G.Synthesizing monitors for safety properties[M]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2002:342-356
[38] Pnueli A.The temporal logic of programs[C]∥18th AnnualSymposium on Foundations of Computer Science,1977.IEEE,1977:46-57
[39] Bauer A,Leucker M,Schallhart C.Monitoring of real-time pro-perties[C]∥FSTTCS 2006:Foundations of Software Technology and Theoretical Computer Science.Springer Berlin Heidelberg,2006:260-272
[40] Bauer A,Leucker M,Schallhart C.Runtime verification for LTL and TLTL[J].ACM Transactions on Software Engineering and Methodology(TOSEM),2011,20(4):14
[41] Maler O,Nickovic D,Pnueli A.From MITL to timed automata[C]∥Formal Modeling and Analysis of Timed Systems.Springer Berlin Heidelberg,2006:274-289
[42] Bauer A,Leucker M,Schallhart C.The good,the bad,and the ugly,but how ugly is ugly?[C]∥Runtime Verification.SpringerBerlin Heidelberg,2007:126-138
[43] Kim C H P,Bodden E,Batory D,et al.Reducing configurations to monitor in a software product line[C]∥Runtime Verification.Springer Berlin Heidelberg,2010:285-299
[44] Bodden E,Lam P.Clara:Partially Evaluating Runtime Monitors at Compile Time[C]∥Runtime Verification.Springer Berlin Heidelberg,2010:74-88
[45] Ehlers R,Finkbeiner B.Monitoring realizability[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:427-441
[46] Basin D,Klaedtke F,Marinovic S,et al.Monitoring compliance policies over incomplete and disagreeing logs[C]∥Runtime Verification.Springer Berlin Heidelberg,2013:151-167
[47] Stoller S D,Bartocci E,Seyster J,et al.Runtime verification with state estimation[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:193-207
[48] Bonakdarpour B,Fischmeister S.Runtime monitoring of time-sensitive systems[C]∥Runtime Verification.Springer Berlin Heidelberg,2012:19-33
[49] Fischmeister S,Lam P.Time-aware instrumentation of embed-ded software[J].IEEE Transactions on Industrial Informatics ,2010,6(4):652-663
[50] Fischmeister S,Lam P.On time-aware instrumentation of programs[C]∥15th IEEE Real-Time and Embedded Technology and Applications Symposium,2009(RTAS 2009).IEEE,2009:305-314
[51] Bartocci E,Grosu R,Karmarkar A,et al.Adaptive runtime verification[C]∥Runtime Verification.Springer Berlin Heidelberg,2013:168-182
[52] Colombo C,Pace G J,Abela P.Compensation-aware runtimemonitoring[C]∥Runtime Verification.Springer Berlin Heidelberg,2010:214-228
[53] Demsky B,Zhou J,Montaz W.Recovery tasks:an automated approach to failure recovery[C]∥Runtime Verification.Springer Berlin Heidelberg,2010:229-244
[54] Colombo C,Pace G J.Fast-Forward Runtime Monitoring－An Industrial Case Study[C]∥Runtime Verification.Springer Berlin Heidelberg,2013:214-228

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed