TY - GEN
T1 - Rule systems for runtime verification
T2 - 9th International Workshop on Runtime Verification, RV 2009
AU - Barringer, Howard
AU - Havelund, Klaus
AU - Rydeheard, David
AU - Groce, Alex
PY - 2009
Y1 - 2009
N2 - In this tutorial, we introduce two rule-based systems for on and off-line trace analysis, RuleR and LogScope. RuleR is a conditional rule-based system, which has a simple and easily implemented algorithm for effective runtime verification, and into which one can compile a wide range of temporal logics and other specification formalisms used for runtime verification. Specifications can be parameterized with data, or even with specifications, allowing for temporal logic combinators to be defined. We outline a number of simple syntactic extensions of core RuleR that can lead to further conciseness of specification but still enabling easy and efficient implementation. RuleR is implemented in Java and we will demonstrate its ease of use in monitoring Java programs. LogScope is a derivation of RuleR adding a simple very user-friendly temporal logic. It was developed in Python, specifically for supporting testing of spacecraft flight software for NASA's next 2011 Mars mission MSL (Mars Science Laboratory). The system has been applied by test engineers to analysis of log files generated by running the flight software. Detailed logging is already part of the system design approach, and hence there is no added instrumentation overhead caused by this approach. While post-mortem log analysis prevents the autonomous reaction to problems possible with traditional runtime verification, it provides a powerful tool for test automation. A new system is being developed that integrates features from both RuleR and LogScope.
AB - In this tutorial, we introduce two rule-based systems for on and off-line trace analysis, RuleR and LogScope. RuleR is a conditional rule-based system, which has a simple and easily implemented algorithm for effective runtime verification, and into which one can compile a wide range of temporal logics and other specification formalisms used for runtime verification. Specifications can be parameterized with data, or even with specifications, allowing for temporal logic combinators to be defined. We outline a number of simple syntactic extensions of core RuleR that can lead to further conciseness of specification but still enabling easy and efficient implementation. RuleR is implemented in Java and we will demonstrate its ease of use in monitoring Java programs. LogScope is a derivation of RuleR adding a simple very user-friendly temporal logic. It was developed in Python, specifically for supporting testing of spacecraft flight software for NASA's next 2011 Mars mission MSL (Mars Science Laboratory). The system has been applied by test engineers to analysis of log files generated by running the flight software. Detailed logging is already part of the system design approach, and hence there is no added instrumentation overhead caused by this approach. While post-mortem log analysis prevents the autonomous reaction to problems possible with traditional runtime verification, it provides a powerful tool for test automation. A new system is being developed that integrates features from both RuleR and LogScope.
KW - Aspectj
KW - Code instrumentation
KW - Java
KW - Log file analysis
KW - Python
KW - Rule systems
KW - Runtime verification
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=70549109220&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70549109220&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-04694-0_1
DO - 10.1007/978-3-642-04694-0_1
M3 - Conference contribution
AN - SCOPUS:70549109220
SN - 3642046932
SN - 9783642046933
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 24
BT - Runtime Verification - 9th International Workshop, RV 2009, Selected Papers
Y2 - 26 June 2009 through 28 June 2009
ER -