Difference between revisions of "Runtime Verification"

From FSL
Jump to: navigation, search
Line 17: Line 17:
 
<purge></purge>
 
<purge></purge>
 
<blockquote>
 
<blockquote>
<pub categories="rv"> </pub>
+
<!--<pub categories="rv"> </pub>-->
 +
<pubbib categories="runtime_verification"/>

Revision as of 04:41, 5 August 2014

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.

Techniques for Evolution-Aware Runtime Verification 
Owolabi Legunsen and Yi Zhang and Milica Hadzi-Tanovic and Grigore Rosu and Darko Marinov
ICST 2019, IEEE, pp 300-311. 2019
PDF, Slides(PPTX), JavaMOP, DOI, ICST 2019, BIB
Runtime Verification at Work: A Tutorial 
Philip Daian and Dwight Guth and Chris Hathhorn and Yilong Li and Edgar Pek and Manasvi Saxena and Traian Florin Serbanuta and Grigore Rosu
RV'16, LNCS 10012, pp 46-67. 2016
PDF, Slides(PPTX), RV Products, DOI, RV'16, BIB
How Good are the Specs? A Study of the Bug-Finding Effectiveness of Existing Java API Specifications 
Owolabi Legunsen and Wajih Ul Hassan and Xinyue Xu and Grigore Rosu and Darko Marinov
ASE 2016, IEEE/ACM, pp 602-613. 2016
PDF, Slides(PDF), JavaMOP, DOI, ASE 2016, BIB
RV-Match: Practical Semantics-Based Program Analysis 
Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
CAV'16, LNCS 9779, pp 447-453. 2016
PDF, RV-Match, DOI, CAV'16, BIB
RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring 
Philip Daian and Bhargava Manja and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu
SAE'16, SAE International 2016-01-0126, pp 1-13. 2016
PDF, Slides(PPT), RV-ECU, DOI, SAE'16, BIB
RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial 
Philip Daian and Ylies Falcone and Patrick Meredith and Traian Florin Serbanuta and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu
RV'15, Lecture Notes in Computer Science 9333, pp 342-357. 2015
PDF, Slides(PDF), RV-Android, DOI, RV'15, BIB
GPredict: Generic Predictive Concurrency Analysis 
Jeff Huang and Qingzhou Luo and Grigore Rosu
ICSE'15, ACM, pp 847-857. 2015
PDF, Slides(PDF), jPredictor, DOI, ICSE'15, BIB
Evolution-Aware Monitoring-Oriented Programming 
Owolabi Legunsen and Darko Marinov and Grigore Rosu
ICSE NIER'15, ACM, pp 615-618. 2015
PDF, Slides(PDF), JavaMOP, DOI, ICSE NIER'15, BIB
ROSRV: Runtime Verification for Robots 
Jeff Huang and Cansu Erdogan and Yi Zhang and Brandon Moore and Qingzhou Luo and Aravind Sundaresan and Grigore Rosu
RV'14, LNCS 8734, pp 247-254. 2014
PDF, Slides(PPTX), Slides(PDF), ROSRV, DOI, RV'14, BIB
RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties 
Qingzhou Luo and Yi Zhang and Choonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Traian Florin Serbanuta and Grigore Rosu
RV'14, LNCS 8734, pp 285-300. 2014
PDF, Slides(PPTX), JavaMOP, DOI, RV'14, BIB
Maximal Sound Predictive Race Detection with Control Flow Abstraction 
Jeff Huang and Patrick Meredith and Grigore Rosu
PLDI'14, ACM, pp 337-348. 2014
PDF, Slides(PPT), Slides(PDF), jPredictor, DOI, PLDI'14, BIB
EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs 
Qingzhou Luo and Grigore Rosu
ISSTA'13, ACM, pp 156-166. 2013
PDF, Slides(PPTX), EnforceMOP, DOI, ISSTA'13, BIB
Efficient Parametric Runtime Verification with Deterministic String Rewriting 
Patrick Meredith and Grigore Rosu
ASE'13, IEEE/ACM, pp 70-80. 2013
PDF, Slides(PPT), Slides(KEY), Slides(PDF), MOP, DOI, ASE'13, BIB
On Safety Properties and Their Monitoring 
Grigore Rosu
SACS, Volume 22(2), pp 327-365. 2012
PDF, MOP, DOI, SACS, BIB
Maximal Causal Models for Sequentially Consistent Systems 
Traian Florin Serbanuta and Feng Chen and Grigore Rosu
RV'12, LNCS 7687, pp 136-150. 2012
PDF, Slides(PDF), JPredictor, DOI, RV'12, BIB
Making Runtime Monitoring of Parametric Properties Practical 
Dongyun Jin
PhD Thesis, University of Illinois at Urbana-Champaign. August 2012
PDF, MOP, DOI, BIB
Efficient, Expressive, and Effective Runtime Verification 
Patrick O'Neil Meredith
PhD Thesis, University of Illinois at Urbana-Champaign. August 2012
PDF, MOP, DOI, BIB
JavaMOP: Efficient Parametric Runtime Monitoring Framework 
Dongyun Jin and Patrick O'Neil Meredith and Choonghwan Lee and Grigore Rosu
ICSE'12, IEEE, pp 1427-1430. 2012
PDF, MOP, DOI, ICSE'12, BIB
Security-Policy Monitoring and Enforcement with JavaMOP 
Soha Hussein and Patrick Meredith and Grigore Rosu
PLAS'12, ACM, pp 3:1-3:11. 2012
PDF, MOP, DOI, PLAS'12, BIB
Scalable Parametric Runtime Monitoring 
Dongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30757, April 2012
PDF, MOP, DOI, BIB
Towards Categorizing and Formalizing the JDK API 
Choonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30006, March 2012
PDF, Java API, DOI, BIB
Semantics and Algorithms for Parametric Monitoring 
Grigore Rosu and Feng Chen
J.LMCS, Volume 8(1), pp 1-47. 2012
PDF, MOP, DOI, J.LMCS, BIB
Maximal Causal Models for Sequentially Consistent Systems 
Traian Florin Serbanuta and Feng Chen and Grigore Rosu
Technical Report http://hdl.handle.net/2142/27708, October 2011
PDF, JPredictor, DOI, BIB
Garbage Collection for Monitoring Parametric Properties 
Dongyun Jin and Patrick O'Neil Meredith and Dennis Griffith and Grigore Rosu
PLDI'11, ACM, pp 415-424. 2011
PDF, Slides(PPTX), Slides(PDF), MOP, DOI, PLDI'11, BIB
An Overview of the MOP Runtime Verification Framework 
Patrick O'Neil Meredith and Dongyun Jin and Dennis Griffith and Feng Chen and Grigore Rosu
J.STTT, Volume 14(3), pp 249-289. 2011
PDF, MOP, DOI, J.STTT, BIB
Runtime Verification with the RV System 
Patrick Meredith and Grigore Rosu
RV'10, Springer, pp 136-152. 2010
PDF, Slides(PPT), Slides(PDF), RV, DOI, RV'10, BIB
Maximal Causal Models for Sequentially Consistent Multithreaded Systems 
Traian Florin Serbanuta and Feng Chen and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17336, September 2010
PDF, JPredictor, DOI, BIB
Monitoring Algorithms for Metric Temporal Logic 
Prasanna Thati and Grigore Rosu
RV'05, Electronic Notes in Theoretical Computer Science 113, pp 145-162. 2005
PDF, MOP, DOI, RV'05, BIB
Rewriting-Based Techniques for Runtime Verification 
Grigore Rosu and Klaus Havelund
J.ASE, Volume 12(2), pp 151-197. 2005
PDF, MOP, DOI, J.ASE, BIB
Generating Optimal Linear Temporal Logic Monitors by Coinduction 
Koushik Sen and Grigore Rosu and Gul Agha
ASIAN'03, Lecture Notes in Computer Science (LNCS) 2896, pp 260-275. 2003
PDF, MOP, DOI, ASIAN'03, BIB
Generating Optimal Monitors for Extended Regular Expressions 
Koushik Sen and Grigore Rosu
RV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 226-245. 2003
PDF, MOP, DOI, RV'03, BIB
Testing Extended Regular Language Membership Incrementally by Rewriting 
Grigore Rosu and Mahesh Viswanathan
RTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 499-514. 2003
PDF, Slides(PPT), MOP, DOI, RTA'03, BIB
Synthesizing Monitors for Safety Properties 
Klaus Havelund and Grigore Rosu
TACAS'02, LNCS 2280, pp 342-356. 2002
PDF, Slides(PPT), MOP, DOI, TACAS'02, BIB
Monitoring Programs using Rewriting 
Klaus Havelund and Grigore Rosu
ASE'01, IEEE, pp 135-143. 2001
PDF, Slides(PPT), MOP, DOI, ASE'01, BIB
Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae 
Grigore Rosu and Klaus Havelund
Technical Report https://ti.arc.nasa.gov/m/pub-archive/archive/0220.pdf, January 2001
PDF, DOI, BIB
Personal tools
Namespaces

Variants
Actions
Navigation