Rule systems for runtime verification: A short tutorial
— Northern Arizona University Skip to main navigation Skip to search Skip to main content Northern Arizona University Home Home Profiles Departments and Centers Scholarly Works Activities Grants Datasets Prizes Search by expertise, name or affiliation Rule systems for runtime verification: A short tutorial Howard Barringer, Klaus Havelund, David Rydeheard, Alex Groce Research output: Chapter in Book/Report/Conference proceeding › Conference contribution 21 Scopus citations Overview Fingerprint Abstract 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. Original language English (US) Title of host publication Runtime Verification - 9th International Workshop, RV 2009, Selected Papers Pages 1-24 Number of pages 24 DOIs https://doi.org/10.1007/978-3-642-04694-0_1 State Published - 2009 Externally published Yes Event 9th International Workshop on Runtime Verification, RV 2009 - Grenoble, France Duration: Jun 26 2009 → Jun 28 2009 Publication series Name Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Volume 5779 LNCS ISSN (Print) 0302-9743 ISSN (Electronic) 1611-3349 Conference Conference 9th International Workshop on Runtime Verification, RV 2009 Country/Territory France City Grenoble Period 6/26/09 → 6/28/09 Keywords Aspectj Code instrumentation Java Log file analysis Python Rule systems Runtime verification Temporal logic ASJC Scopus subject areas Theoretical Computer Science Computer Science(all) Access to Document 10.1007/978-3-642-04694-0_1 Other files and links Link to publication in Scopus Fingerprint Dive into the research topics of 'Rule systems for runtime verification: A short tutorial'. Together they form a unique fingerprint. Runtime Verification Mathematics 100% Ruler Mathematics 75% Temporal logic Engineering & Materials Science 46% Specifications Engineering & Materials Science 33% Specification Mathematics 31% Temporal Logic Mathematics 31% Rule-based Systems Mathematics 28% Knowledge based systems Engineering & Materials Science 28% View full fingerprint Cite this APA Standard Harvard Vancouver Author BIBTEX RIS Barringer, H., Havelund, K., Rydeheard, D., & Groce, A. (2009). Rule systems for runtime verification: A short tutorial. In Runtime Verification - 9th International Workshop, RV 2009, Selected Papers (pp. 1-24). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5779 LNCS). https://doi.org/10.1007/978-3-642-04694-0_1 Rule systems for runtime verification : A short tutorial. / Barringer, Howard; Havelund, Klaus; Rydeheard, David; Groce, Alex. Runtime Verification - 9th International Workshop, RV 2009, Selected Papers. 2009. p. 1-24 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5779 LNCS). Research output: Chapter in Book/Report/Conference proceeding › Conference contribution Barringer, H, Havelund, K, Rydeheard, D & Groce, A 2009, Rule systems for runtime verification: A short tutorial. in Runtime Verification - 9th International Workshop, RV 2009, Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5779 LNCS, pp. 1-24, 9th International Workshop on Runtime Verification, RV 2009, Grenoble, France, 6/26/09. https://doi.org/10.1007/978-3-642-04694-0_1 Barringer H, Havelund K, Rydeheard D, Groce A. Rule systems for runtime verification: A short tutorial. In Runtime Verification - 9th International Workshop, RV 2009, Selected Papers. 2009. p. 1-24. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-04694-0_1 Barringer, Howard ; Havelund, Klaus ; Rydeheard, David ; Groce, Alex. / Rule systems for runtime verification : A short tutorial. Runtime Verification - 9th International Workshop, RV 2009, Selected Papers. 2009. pp. 1-24 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). @inproceedings{f8ffe1b39e7a43b194a76fbc23be913b, title = "Rule systems for runtime verification: A short tutorial", abstract = "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.", keywords = "Aspectj, Code instrumentation, Java, Log file analysis, Python, Rule systems, Runtime verification, Temporal logic", author = "Howard Barringer and Klaus Havelund and David Rydeheard and Alex Groce", year = "2009", doi = "10.1007/978-3-642-04694-0_1", language = "English (US)", isbn = "3642046932", series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)", pages = "1--24", booktitle = "Runtime Verification - 9th International Workshop, RV 2009, Selected Papers", note = "9th International Workshop on Runtime Verification, RV 2009 ; Conference date: 26-06-2009 Through 28-06-2009", } 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 - Powered by Pure, Scopus & Elsevier Fingerprint Engine™ © 2022 Elsevier B.V We use cookies to help provide and enhance our service and tailor content. By continuing you agree to the use of cookies Log in to Pure About web accessibility Contact us
