Abstract
In this paper we introduce JMSeq, a Java-based tool for the specification and runtime verification via monitoring of sequences of possibly nested method calls. JMSeq provides a simple but expressive way to specify the sequential execution of a Java program using code annotations via user-given sequences of methods calls. Similar to many monitoring-oriented environments, verification in JMSeq is done at run-time, but differently from all other approaches based on aspect-oriented programming, JMSeq does not use code instrumentation, and therefore is suitable for component-based software verification.
This research is partly funded by the EU project FP7-231620 HATS: Highly Adaptable and Trustworthy Software using Formal Models ( http://www.hats-project.eu/ )
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.
Similar content being viewed by others
References
AspectJ Language Semantics, http://eclipse.org/aspectj/doc/released/progguide/semantics-pointcuts.html
Eclipse Debug Platform, http://www.eclipse.org/eclipse/debug/
Java 5 Annotations, http://java.sun.com/j2se/1.5.0/docs/guide/language/annotations.html
JPDA Reference Home Page, http://java.sun.com/javase/technologies/core/toolsapis/jpda/
JUnit Test Framework, http://www.junit.org/
MOP: Monitoring-oriented programming, http://fsl.cs.uiuc.edu/index.php/MOP
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhotak, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA (2005)
Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56, 16:1–16:43 (2009)
Anercrombie, P., Karaorman, M.: jContractor: Bytecode instrumentation techniques for implementing dbc in Java. In: RV 2002 (2002)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: VMCI 2004 (2004)
Bartetzko, D., Fischer, C., Moller, M., Wehrheim, H.: Jass - Java with Assertions. In: RV 2001 (2001)
Bodden, E.: J-lo, a tool for runtime-checking temporal assertions. Master Thesis, RWTH Aachen University (2005)
Chen, F., Rosu, G.: Towards Monitoring-Oriented programming: A paradigm combining specification and implementation. Electronic Notes in Theoretical Computer Science 89(2), 108–127 (2003)
Chen, F., Rosu, G.: Java-MOP: A monitoting oriented programming environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005)
Chen, F., Rosu, G.: MOP: An Efficient and Generic Runtime Verification Framework. In: OOPSLA. ACM Press, New York (2007)
Cheon, Y., Perummandla, A.: Specifying and checking method call sequences of Java programs. Software Qual J. 15, 7–25 (2007)
de Gouw, S., Vinju, J., de Boer, F.S.: Prototyping a tool environment for run-time assertion checking in JML with Communication Histories. In: FTfJP 2010 (2010)
Havelund, K., Rosu, G.: Monitoring Java programs with Java PathExplorer. In: RV 2001 (2001)
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.: Getting started with ASPECTJ. In: ACM CACM (2001)
Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a Runtime Assurance Tool for Java. In: RV 2001 (2001)
Knuth, D.E.: Semantics of context-free languages. Mathematical Systems Theory 2(2), 127–145 (1968)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary Design of JML: A Behavioral Interface Specification Language for Java. ACM SIGSOFT Software Engineering (2006)
Martin, M., Livshits, V.B., Lam, M.S.: Finding application erros and security flaws using PQL: a program query language. In: OOPSLA (2005)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, New Jersey (2000)
Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 106–119. ACM, New York (1997)
Rebelo, H., Soares, S., Lima, R., Borba, P., Cornelio, M.: JML and Aspects: The benefits of instrumenting JML features with AspectJ (2008)
Szyperski, C., Gruntz, D., Murer, S.: Component software: beyond object-oriented programming. Addison-Wesley, Reading (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nobakht, B., Bonsangue, M.M., de Boer, F.S., de Gouw, S. (2012). Monitoring Method Call Sequences Using Annotations. In: Barbosa, L.S., Lumpe, M. (eds) Formal Aspects of Component Software. FACS 2010. Lecture Notes in Computer Science, vol 6921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27269-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-27269-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27268-4
Online ISBN: 978-3-642-27269-1
eBook Packages: Computer ScienceComputer Science (R0)