Abstract
Monitoring-Oriented Programming (MOP1) [21, 18, 22, 19] is a formal framework for software development and analysis, in which the developer specifies desired properties using definable specification formalisms, along with code to execute when properties are violated or validated. The MOP framework automatically generates monitors from the specified properties and then integrates them together with the user-defined code into the original system.
The previous design of MOP only allowed specifications without parameters, so it could not be used to state and monitor safety properties referring to two or more related objects. In this paper we propose a parametric specification formalism-independent extension of MOP, together with an implementation of JavaMOP that supports parameters. In our current implementation, parametric specifications are translated into AspectJ code and then weaved into the application using off-the-shelf AspectJ compilers; hence, MOP specifications can be seen as formal or logical aspects.
Our JavaMOP implementation was extensively evaluated on two benchmarks, Dacapo [14] and Tracematches [8], showing that runtime verification in general and MOP in particular are feasible. In some of the examples, millions of monitor instances are generated, each observing a set of related objects. To keep the runtime overhead of monitoring and event observation low, we devised and implemented a decentralized indexing optimization. Less than 8% of the experiments showed more than 10% runtime overhead; in most cases our tool generates monitoring code as efficient as the hand-optimized code. Despite its genericity, JavaMOP is empirically shown to be more efficient than runtime verification systems specialized and optimized for particular specification formalisms. Many property violations were detected during our experiments; some of them are benign, others indicate defects in programs. Many of these are subtle and hard to find by ordinary testing.
- P. Abercrombie and M. Karaorman. jContractor: Bytecode instrumentation techniques for implementing DBC in Java. In RV'02, volume 70.4 of ENTCS, 2002Google Scholar
- C. Allan, P. Avgustinov, A. S. Christensen, L. Hendren, S. Kuzins, O. Lhotak, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. Adding trace matching with free variables to AspectJ. In OOPSLA'05, 2005. Google ScholarDigital Library
- C. Anley. Advanced SQL injection in SQL server applications. NGSSoftware, 2002.Google Scholar
- AspectC++. http://www.aspectc.org/.Google Scholar
- C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, and W. Visser. Experiments with test case generation and runtime analysis. In ASM'03, volume 2589 of LNCS, pages 87--107, 2003. Google ScholarDigital Library
- P. Avgustinov, E. Bodden, E. Hajiyev, L. Hendren, O. Lhotak, O. de Moor, N. Ongkingco, D. Sereni, G. Sittampalam, J. Tibble, and M. Verbaere. Aspects for trace monitoring. In FATES/RV'06, volume 4262 of LNCS, pages 20--39, 2006. Google ScholarDigital Library
- P. Avgustinov, A. S. Christensen, L. Hendren, S. Kuzins, J. Lhotak, O. Lhotak, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. ABC: an extensible AspectJ compiler. In AOSD'05, 2005. Google ScholarDigital Library
- P. Avgustinov, J. Tibble, E. Bodden, O. Lhotak, L. Hendren, O. de Moor, N. Ongkingco, and G. Sittampalam. Efficient Trace Monitoring. Technical Report abc-2006-1, Oxford University, 2006.Google ScholarDigital Library
- P. Avgustinov, J. Tibble, and O. de Moor. Making Trace Monitors Feasible. In OOPSLA'07, 2007. this volume. Google ScholarDigital Library
- M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS'04, volume 3362 of LNCS, pages 49--69, 2004. Google ScholarDigital Library
- H. Barringer, B. Finkbeiner, Y. Gurevich, and H. Sipma. Runtime Verification (RV'05). Elsevier, 2005. ENTCS 144.Google Scholar
- H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-Based Runtime Verification. In VMCAI'04, volume 2937 of LNCS, pages 44--57, 2004.Google Scholar
- D. Bartetzko, C. Fischer, M. Moller, and H. Wehrheim. Jass-Java with Assertions. In RV'01, volume 55.2 of ENTCS, 2001.Google Scholar
- S. M. Blackburn, R. Garner, C. Hoffman, A. M. Khan, K. S. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Z. Guyer, M. Hirzel, A. Hosking, M. Jump, H. Lee, J. E. B. Moss, A. Phansalkar, D. Stefanovi2c, T. VanDrunen, D. von Dincklage, and B. Wiedermann. The DaCapo benchmarks: Java benchmarking development and analysis. In OOPSLA'06, 2006. Google ScholarDigital Library
- E. Bodden. J-LO, a tool for runtime-checking temporal assertions. PhD thesis, RWTH Aachen University, 2005.Google Scholar
- E. Bodden, L. Hendren, and O. Lhot2ak. A staged static program analysis to improve the performance of runtime monitoring. In ECOOP'07, volume 4609 of LNCS, pages 525--549, 2007. Google ScholarDigital Library
- E. Bodden, P. Lam, and L. Hendren. Flow-sensitive static optimizations for runtime monitors. Technical Report abc-2007-3, Oxford University, 2007.Google Scholar
- F. Chen, M. D'Amorim, and G. Roşu. A formal monitoringbased framework for software development and analysis. In ICFEM'04, volume 3308 of LNCS, pages 357--373, 2004.Google Scholar
- F. Chen, M. D'Amorim, and G. Roşu. Checking and correcting behaviors of Java programs at runtime with JavaMOP. In RV'05, volume 144(4) of ENTCS, 2005. Google ScholarDigital Library
- F. Chen and G. Roşu. JavaMOP. http://fsl.cs.uiuc.edu/javamop.Google Scholar
- F. Chen and G. Roşu. Towards monitoring-oriented programming: A paradigm combining specification and implementation. In RV'03, volume 89(2) of ENTCS, 2003.Google Scholar
- F. Chen and G. Roşu. Java-MOP: A monitoring oriented programming environment for Java. In TACAS'05, volume 3440 of LNCS, pages 546--550, 2005. Google ScholarDigital Library
- M. d'Amorim and K. Havelund. Event-based runtime verification of Java programs. In International Workshop on Dynamic analysis (WODA'05), 2005. Google ScholarDigital Library
- D. Drusinsky. Temporal Rover. http://www.time-rover.com.Google Scholar
- Eclipse. http://eclipse.org.Google Scholar
- Eiffel Language. http://www.eiffel.com/.Google Scholar
- S. Goldsmith, R. O'Callahan, and A. Aiken. Relational queries over program traces. In OOPSLA'05, 2005. Google ScholarDigital Library
- K. Havelund and G. Roşu. Monitoring Java programs with Java PathExplorer. In RV'01, volume 55.2 of ENTCS, 2001.Google Scholar
- K. Havelund and G. Roşu. Runtime Verification (RV'01, RV'02, RV'04). Elsevier, 2001, 2002, 2004. ENTCS 55, 70,113.Google Scholar
- C. Hoare. Communicating Sequential Processes. Prentice-Hall Intl., New York, 1985. Google ScholarDigital Library
- JBoss. http://www.jboss.org.Google Scholar
- jHotdraw. http://www.jhotdraw.org.Google Scholar
- G. Kiczales, J. Lamping, A. Menhdhekar, C. Maeda, C. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-Oriented programming. In ECOOP'97, volume 1241 of LNCS, pages 220--242, 1997.Google Scholar
- G. Kiczales, J. D. Rivieres, and D. G. Bobrow. The Art of the Metaobject Protocol. MIT Press, 1991. Google ScholarDigital Library
- M. Kim, S. Kannan, I. Lee, and O. Sokolsky. Java-MaC: a Runtime Assurance Tool for Java. In RV'01, volume 55.2 of ENTCS, 2001.Google Scholar
- G. T. Leavens, K. R. M. Leino, E. Poll, C. Ruby, and B. Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA'00, 2000. Google ScholarDigital Library
- Lucene. http://lucene.apache.org.Google Scholar
- M. Martin, V. B. Livshits, and M. S. Lam. Finding application errors and security flaws using PQL: a program query language. In OOPSLA'05, 2005. Google ScholarDigital Library
- B. Meyer. Object-Oriented Software Construction, 2nd edition. Prentice Hall, New Jersey, 2000. Google ScholarDigital Library
- M. Rinard. Acceptability-oriented computing. In Onward! Track, OOPSLA'03, 2003. Google ScholarDigital Library
- O. Sokolsky and M. Viswanathan. Runtime Verification (RV'03). Elsevier, 2003. ENTCS 89.Google Scholar
- Xalan. http://xml.apache.org/xalan-j/.Google Scholar
Index Terms
- Mop: an efficient and generic runtime verification framework
Recommendations
Mop: an efficient and generic runtime verification framework
OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applicationsMonitoring-Oriented Programming (MOP1) [21, 18, 22, 19] is a formal framework for software development and analysis, in which the developer specifies desired properties using definable specification formalisms, along with code to execute when properties ...
An overview of the MOP runtime verification framework
This article gives an overview of the, monitoring oriented programming framework (MOP). In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable systems. Monitors are automatically synthesized from ...
Efficient and expressive bytecode-level instrumentation for Java programs
AbstractWe present an efficient and expressive tool for the instrumentation of Java programs at the bytecode level. BISM (Bytecode-Level Instrumentation for Software Monitoring) is a lightweight Java bytecode instrumentation tool that features an ...
Comments