Runtime Verification

From FSL
Revision as of 14:18, 31 August 2011 by Grosu (Talk | contribs)

Jump to: navigation, search

Runtime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications. Runtime verification specifications are typically expressed in trace predicate formalisms, such as finite state machines, regular expressions, context-free patterns, linear temporal logics, etc., or extensions of these. This allows for a less adhoc approach than normal testing. However, any mechanism for monitoring an executing system is considered runtime verification, including verifying against test oracles and reference implementations. When formal requirements specifications are provided, monitors are synthesized from them and infused within the system by means of instrumentation. Runtime verification can be used for many purposes, such as security or safety policy monitoring, debugging, testing, verification, validation, profiling, fault protection, behavior modification (e.g., recovery), etc. Runtime verification avoids the complexity of traditional formal verification techniques, such as model checking and theorem proving, by analyzing only one or a few execution traces and by working directly with the actual system, thus scaling up relatively well and giving more confidence in the results of the analysis (because it avoids the tedious and error-prone step of formally modelling the system), at the expense of less coverage. Moreover, through its reflective capabilities runtime verification can be made an integral part of the target system, monitoring and guiding its execution during deployment.

The terminology runtime verification was formally introduced as the name of a 2001 workshop, organized by Klaus Havelund and Grigore Rosu, aimed at addressing problems at the boundary between formal verification and testing. For more information and examples, we refer the interested reader to the Wikipedia runtime verification page:

Wikipedia Runtime Verification.

FSL Research on Runtime Verification

We do runtime verification research on the following specific topics:

FSL Publications on Runtime Verification

Below is the list of all our publications that are directly or indirectly related to runtime verification, in reverse chronological order. If interested in publications on specific topics then click on the links above.

Maximal Causal Models for Sequentially Consistent Systems 
Traian Florin Serbanuta, Feng Chen and Grigore Rosu
RV'12, LNCS. 7687, pp 136-150. 2013
PDF, Slides(PDF), BIB
Efficient, Expressive, and Effective Runtime Verification 
Patrick Meredith
PhD Thesis, University of Illinois, August 2012
PDF, Slides(KEY), Slides(PDF), JavaMOP Project, BusMOP Project, RV-Predict Project, BIB
Security-Policy Monitoring and Enforcement with JavaMOP 
Soha Hussein, Patrick Meredith and Grigore Rosu
PLAS'12, ACM, pp 3:1-3:11. 2012
PDF, Slides(KEY), Slides(PDF), ACM, PLAS'12, BIB
Scalable Parametric Runtime Monitoring 
Dongyun Jin, Patrick Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30757, April 2012
PDF, TR@UIUC, BIB
JavaMOP: Efficient Parametric Runtime Monitoring Framework 
Dongyun Jin, Patrick Meredith, Choonghwan Lee and Grigore Rosu
ICSE'12, IEEE, pp 1427-1430. 2012
PDF, Demo Movie, TOOL ICSE'12, BIB
Towards Categorizing and Formalizing the JDK API 
Choonghwan Lee, Dongyun Jin, Patrick Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30006, March 2012
PDF, TR@UIUC, BIB
Semantics and Algorithms for Parametric Monitoring 
Grigore Rosu and Feng Chen
J.LMCS, Volume 8(1), pp 1-47. 2012
PDF, MOP, J.LMCS, BIB
Improved Multithreaded Unit Testing 
Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu and Darko Marinov
FSE'11, ACM, pp 223-233. 2011
PDF, FSE'11, BIB
Garbage Collection for Monitoring Parametric Properties 
Dongyun Jin, Patrick Meredith, Dennis Griffith and Grigore Rosu
PLDI'11, ACM, pp 415-424. 2011
PDF, PLDI'11 slides(pptx), PLDI'11 slides(pdf), ACM, PLDI'11, JavaMOP, BIB
Mining Parametric Specifications 
Choonghwan Lee, Feng Chen and Grigore Rosu
ICSE'11, ACM, pp 591-600. 2011
PDF, Slides(pptx), ACM, ICSE'11, jMiner, BIB
An Overview of the MOP Runtime Verification Framework 
Patrick Meredith, Dongyun Jin, Dennis Griffith, Feng Chen and Grigore Rosu
J.STTT, http://dx.doi.org/10.1007/s10009-011-0198-6
PDF, J.STTT, BIB
A Rewriting Approach to Concurrent Programming Language Design and Semantics 
Traian Florin Serbanuta
PhD Thesis, University of Illinois, December 2010
PDF, Slides (PDF), K-Maude, TR@UIUC, BIB
Runtime Verification with the RV System 
Patrick Meredith and Grigore Rosu
RV'10, LNCS 6418, pp 136-152. 2010
PDF, Slides(PDF), Slides(PPT), Slides(KEY), RV'10, BIB
Efficient Monitoring of Parametric Context-Free Patterns 
Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
J. of ASE, Volume 17(2), pp 149-180. 2010
PDF, J.ASE, BIB
Efficient Formalism-Independent Monitoring of Parametric Properties 
Feng Chen, Patrick Meredith, Dongyun Jin and Grigore Rosu
ASE'09, IEEE/ACM, pp 383-394. 2009
PDF, ASE'09 slides(KEY), ASE'09 slides(PDF), IEEE, ASE'09, BIB
Handling Mixed-Criticality in SoC-based Real-Time Embedded Systems 
Rodolfo Pellizzoni, Patrick Meredith, Min-Young Nam, Mu Sun, Marco Caccamo and Lui Sha
Emsoft'09, ACM, pp 235--244. 2009
PDF, Slides(PPTX), ACM, Emsoft'09, BIB
Runtime Verification of C Memory Safety 
Grigore Rosu, Wolfram Schulte and Traian Florin Serbanuta
RV'09, LNCS 5779, pp 132-151. 2009
PDF, Slides (PDF), LNCS, RV'09, BIB
Monitoring Oriented Programming - A Project Overview 
Feng Chen, Dongyun Jin, Patrick Meredith, and Grigore Rosu
ICICIS'09, pp 72-77. 2009
PDF, ICICIS'09, BIB
Parametric Trace Slicing and Monitoring 
Feng Chen and Grigore Rosu
TACAS'09, LNCS 5505, pp 246-261. 2009.
PDF, Slides (PPT), LNCS, TACAS'09, DBLP, BIB
Dependent advice: A general approach to optimizing history-based Aspects 
Eric Bodden, Feng Chen and Grigore Rosu
AOSD'09, ACM, pp 3--14. 2009.
PDF, ACM, AOSD'09, TR@ABC, BIB
Hardware Runtime Monitoring for Dependable COTS-based Real-Time Embedded Systems 
Rodolfo Pellizzoni, Patrick Meredith, Marco Caccamo and Grigore Rosu
RTSS'08, IEEE, pp. 481-491. 2008
PDF, Experiments, Slides(PPTX), IEEE, RTSS'08, BIB
Monitoring IVHM Systems using a Monitor-Oriented Programming Framework 
Sudipto Ghoshal, Solaiappan Manimaran, Grigore Rosu, Traian Florin Serbanuta, and Gheorghe Stefanescu
LFM 2008
PDF, Slides (PPT), LFM'08, BIB
Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns -- 
Grigore Rosu, Feng Chen and Thomas Ball
RV'08, LNCS 5289, pp 51-68, 2008
PDF, RV'08, BIB
Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns -- 
Grigore Rosu,Feng Chen and Thomas Ball
Technical report UIUCDCS-R-2007-2908, October 2007
PDF, BIB
MOP: An Efficient and Generic Runtime Verification Framework 
Feng Chen and Grigore Rosu
OOPSLA'07, ACM press, pp 569-588. 2007
PDF, OOPSLA'07 slides, ACM, OOPSLA'07, DBLP, TR@UIUC, BIB
On Safety Properties and Their Monitoring 
Grigore Rosu
Technical report UIUCDCS-R-2007-2850, February 2007
PDF, ZIP, TR@UIUC, BIB
Allen Linear (Interval) Temporal Logic -Translation to LTL and Monitor Synthesis- 
Grigore Rosu and Saddek Bensalem
CAV'06, LNCS 4144, pp 263-277, 2006
PDF, CAV'06, CAV'06 Slides, BIB
Efficient Monitoring of Omega-Languages 
Marcelo d'Amorim and Grigore Rosu
CAV'05, LNCS 3576, pp 364 - 378. 2005.
PDF, LNCS, CAV'05, DBLP, BIB
Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP 
Feng Chen, Marcelo d'Amorim and Grigore Rosu
RV'05, ENTCS 144, issue 4, pp 3-20. 2005.
PDF, ENTCS, RV'05, DBLP, BIB
Predicting Concurrency Errors at Runtime using Sliced Causality 
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2005-2660, 2005.
PDF, TR@UIUC, BIB
Java-MOP: A Monitoring Oriented Programming Environment for Java 
Feng Chen and Grigore Rosu
TACAS'05, LNCS 3440, pp 546-550. 2005.
PDF, LNCS, TACAS'05, DBLP, BIB
Rewriting-based Techniques for Runtime Verification 
Grigore Rosu and Klaus Havelund
J.ASE, Volume 12(2), pp 151-197. 2005
PDF, J.ASE, DBLP, BIB
Efficient Monitoring of Safety Properties 
Klaus Havelund and Grigore Rosu
J. of STTT, Volume 6(2), pp 158-173. 2004
PDF, J.STTT, BIB
Monitoring-Oriented Programming: A Tool-Supported Methodology for Higher Quality Object-Oriented Software 
Feng Chen, Marcelo d'Amorim and Grigore Rosu
Technical Report UIUCDCS-R-2004-2420, 2004.
PDF, TR@UIUC, BIB
A Formal Monitoring-based Framework for Software Development and Analysis 
Feng Chen and Marcelo d'Amorim and Grigore Rosu
ICFEM'04, LNCS 3308, pp 357 - 373. 2004.
PDF, LNCS, ICFEM'04, DBLP, BIB
Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation 
Feng Chen and Grigore Rosu
RV'03, ENTCS 89, issue 2, pp 108 - 127. 2003.
PDF, ENTCS, RV'03, DBLP, BIB
Personal tools
Namespaces

Variants
Actions
Navigation