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.
Part of the research described in this publication was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittamplan, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA 2005. ACM Press, New York (2005)
Andrews, J.H., Zhang, Y.: General test result checking with log file analysis. IEEE Transactions on Software Engineering 29(7), 634–648 (2003)
Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62–74. Springer, Heidelberg (1989)
Barringer, H., Fisher, M., Gabbay, D., Gough, G., Owens, R.: MetateM: an introduction. Formal Aspects of Computing 7(5), 533–549 (1995)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 111–125. Springer, Heidelberg (2007)
Barringer, H., Rydeheard, D., Havelund, K.: RuleR: A tutorial guide (2008), http://www.cs.man.ac.uk/~howard/LPA.html
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. Journal of Logic and Computation (2009), Advance Access published on November 21 (2008), doi:10.1093/logcom/exn076
Chen, F., Roşu, G.: MOP: An efficient and generic runtime verification framework. In: Object-Oriented Programming, Systems, Languages and Applications, OOPSLA 2007 (2007)
Drusinsky, D.: Modeling and Verification using UML Statecharts, 400 pages. Elsevier, Amsterdam (2006)
Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) TestCom/FATES 2008. LNCS, vol. 5047, pp. 7–22. Springer, Heidelberg (2008)
Hodkinson, I.M., Reynolds, M.: Separation - past, present, and future. In: Artëmov, S.N., Barringer, H., d’Avila Garcez, A.S., Lamb, L.C., Woods, J. (eds.) We Will Show Them! vol. 2, pp. 117–142. College Publications (2005)
Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance tool for Java. In: Proc. of the 1st International Workshop on Runtime Verification (RV 2001). ENTCS, vol. 55(2). Elsevier, Amsterdam (2001)
Lange, M.: Alternating context-free languages and linear time mu-calculus with sequential composition. Electr. Notes Theor. Comput. Sci. 68(2) (2002)
Moszkowski, B.: Executing temporal logic programs. Cambridge University Press, Cambridge (1980)
Moszkowski, B.C., Manna, Z.: Reasoning in interval temporal logic. In: Clarke, E.M., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 371–382. Springer, Heidelberg (1984)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE Computer Society, Los Alamitos (1977)
Smith, M., Havelund, K.: Requirements capture with RCAT. In: 16th IEEE International Requirements Engineering Conference (RE 2008). IEEE Computer Society, Barcelona (2008)
Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: Proc. of the 5th International Workshop on Runtime Verification (RV 2005). ENTCS, vol. 144(4). Elsevier, Amsterdam (2005)
Sun Microsystems, Inc. Java Platform, Standard Edition 6, API Specification (2009), http://java.sun.com/javase/6/docs/api/
Wolper, P.: Temporal logic can be more expressive. Information and Control 56 (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barringer, H., Havelund, K., Rydeheard, D., Groce, A. (2009). Rule Systems for Runtime Verification: A Short Tutorial. In: Bensalem, S., Peled, D.A. (eds) Runtime Verification. RV 2009. Lecture Notes in Computer Science, vol 5779. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04694-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-04694-0_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04693-3
Online ISBN: 978-3-642-04694-0
eBook Packages: Computer ScienceComputer Science (R0)