ruler-tutorial

RuleR: A Tutorial GuideDRAFT: Version 0.11Howard Barringer, David RydeheardSchool of Computer ScienceUniversity of ManchesterOxford RoadManchester, M13 9PL, UKemail: {Howard.Barringer, David.Rydeheard}@manchester.ac.ukKlaus HavelundNASA’s Jet Propulsion LaboratoryCalifornia Institute of TechnologyPasadena, CA 91109, USAemail: Klaus.Havelund@jpl.nasa.govJune 30, 2008AbstractRuleR was introduced as a primitive conditional rule-based system, which we claim can beefficientlyimplementedforrun-timechecking, andintowhichonecancompilevarioustemporallogicsused for run-time verification. RuleR was created in the spirit of Eagle but has a considerablyeasier semantics. Although our original goals positioned RuleR as a low-level target rule-system foreasy interpretation, following a prototype Java implementation of RuleR incorporating data andrule parameters, we have since enhanced RuleR to support its direct use as a monitor specificationsystem. This tutorial takes the reader on a tour through the current system, its enhancements over“core” RuleR and examples of its use in monitoring Java programs instrumented using AspectJ.We recommend, however, that the paper [2] is read first.RuleR remains an experimental system with an implementation that evolves freely with thewhim of its originators. Not all of its features (including bugs) are documented.KeywordsRun-time verification, rule systems, temporal logic, grammars, Java, AspectJ.1 ...