skip to main content
article

Mop: an efficient and generic runtime verification framework

Authors Info & Claims
Published:21 October 2007Publication History
Skip Abstract Section

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.

References

  1. P. Abercrombie and M. Karaorman. jContractor: Bytecode instrumentation techniques for implementing DBC in Java. In RV'02, volume 70.4 of ENTCS, 2002Google ScholarGoogle Scholar
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. C. Anley. Advanced SQL injection in SQL server applications. NGSSoftware, 2002.Google ScholarGoogle Scholar
  4. AspectC++. http://www.aspectc.org/.Google ScholarGoogle Scholar
  5. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  6. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  7. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. P. Avgustinov, J. Tibble, and O. de Moor. Making Trace Monitors Feasible. In OOPSLA'07, 2007. this volume. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  11. H. Barringer, B. Finkbeiner, Y. Gurevich, and H. Sipma. Runtime Verification (RV'05). Elsevier, 2005. ENTCS 144.Google ScholarGoogle Scholar
  12. 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 ScholarGoogle Scholar
  13. D. Bartetzko, C. Fischer, M. Moller, and H. Wehrheim. Jass-Java with Assertions. In RV'01, volume 55.2 of ENTCS, 2001.Google ScholarGoogle Scholar
  14. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  15. E. Bodden. J-LO, a tool for runtime-checking temporal assertions. PhD thesis, RWTH Aachen University, 2005.Google ScholarGoogle Scholar
  16. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  17. E. Bodden, P. Lam, and L. Hendren. Flow-sensitive static optimizations for runtime monitors. Technical Report abc-2007-3, Oxford University, 2007.Google ScholarGoogle Scholar
  18. 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 ScholarGoogle Scholar
  19. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  20. F. Chen and G. Roşu. JavaMOP. http://fsl.cs.uiuc.edu/javamop.Google ScholarGoogle Scholar
  21. 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 ScholarGoogle Scholar
  22. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  23. M. d'Amorim and K. Havelund. Event-based runtime verification of Java programs. In International Workshop on Dynamic analysis (WODA'05), 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. D. Drusinsky. Temporal Rover. http://www.time-rover.com.Google ScholarGoogle Scholar
  25. Eclipse. http://eclipse.org.Google ScholarGoogle Scholar
  26. Eiffel Language. http://www.eiffel.com/.Google ScholarGoogle Scholar
  27. S. Goldsmith, R. O'Callahan, and A. Aiken. Relational queries over program traces. In OOPSLA'05, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. K. Havelund and G. Roşu. Monitoring Java programs with Java PathExplorer. In RV'01, volume 55.2 of ENTCS, 2001.Google ScholarGoogle Scholar
  29. K. Havelund and G. Roşu. Runtime Verification (RV'01, RV'02, RV'04). Elsevier, 2001, 2002, 2004. ENTCS 55, 70,113.Google ScholarGoogle Scholar
  30. C. Hoare. Communicating Sequential Processes. Prentice-Hall Intl., New York, 1985. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. JBoss. http://www.jboss.org.Google ScholarGoogle Scholar
  32. jHotdraw. http://www.jhotdraw.org.Google ScholarGoogle Scholar
  33. 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 ScholarGoogle Scholar
  34. G. Kiczales, J. D. Rivieres, and D. G. Bobrow. The Art of the Metaobject Protocol. MIT Press, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. 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 ScholarGoogle Scholar
  36. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  37. Lucene. http://lucene.apache.org.Google ScholarGoogle Scholar
  38. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  39. B. Meyer. Object-Oriented Software Construction, 2nd edition. Prentice Hall, New Jersey, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  40. M. Rinard. Acceptability-oriented computing. In Onward! Track, OOPSLA'03, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  41. O. Sokolsky and M. Viswanathan. Runtime Verification (RV'03). Elsevier, 2003. ENTCS 89.Google ScholarGoogle Scholar
  42. Xalan. http://xml.apache.org/xalan-j/.Google ScholarGoogle Scholar

Index Terms

  1. Mop: an efficient and generic runtime verification framework

            Recommendations

            Comments

            Login options

            Check if you have access through your login credentials or your institution to get full access on this article.

            Sign in

            Full Access

            • Published in

              cover image ACM SIGPLAN Notices
              ACM SIGPLAN Notices  Volume 42, Issue 10
              Proceedings of the 2007 OOPSLA conference
              October 2007
              686 pages
              ISSN:0362-1340
              EISSN:1558-1160
              DOI:10.1145/1297105
              Issue’s Table of Contents
              • cover image ACM Conferences
                OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications
                October 2007
                728 pages
                ISBN:9781595937865
                DOI:10.1145/1297027

              Copyright © 2007 ACM

              Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

              Publisher

              Association for Computing Machinery

              New York, NY, United States

              Publication History

              • Published: 21 October 2007

              Check for updates

              Qualifiers

              • article

            PDF Format

            View or Download as a PDF file.

            PDF

            eReader

            View online with eReader.

            eReader