Computer Science ›› 2014, Vol. 41 ›› Issue (Z11): 359-363.

Previous Articles     Next Articles

Research Advances in Runtime Verification

ZHANG Shuo and HE Fei   

  • Online:2018-11-14 Published:2018-11-14

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

[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

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!