Abstract
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 specified properties and are used in conjunction with the original system to check its dynamic behaviors. When a specification is violated or validated at runtime, user-defined actions will be triggered, which can be any code, such as information logging or runtime recovery. Two instances of MOP are presented: JavaMOP (for Java programs) and BusMOP (for monitoring PCI bus traffic). The architecture of MOP is discussed, and an explanation of parametric trace monitoring and its implementation is given. A comprehensive evaluation of JavaMOP attests to its efficiency, especially in comparison with similar systems. The implementation of BusMOP is discussed in detail. In general, BusMOP imposes no runtime overhead on the system it is monitoring.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abercrombie, P., Karaorman, M.: jContractor: Bytecode instrumentation techniques for implementing DBC in Java. In Runtime Verification (RV’02), ENTCS, vol. 70, Elsevier, Amsterdam (2002)
Aho A.V., Sethi R., Ullman J.D.: Compilers, Principles, Techniques, and Tools, pp. 215–246. Addison-Wesley, New York (1986)
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’05), pp. 345–364. ACM, New York (2005)
Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04), LNCS, vol. 2988, pp. 467–481. Springer, Berlin (2004)
AspectC++. http://www.aspectc.org/
AspectJ. http://eclipse.org/aspectj/
Avgustinov, P., Tibble, J., de Moor, O.: Making trace monitors feasible. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’07), pp. 589–608. ACM, New York (2007)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS’04), LNCS, vol. 3362, pp. 49–69. Springer, Berlin (2004)
Barringer, H., Finkbeiner, B., Gurevich, Y., Sipma, H. (eds): Runtime Verification (RV’05), ENTCS, vol. 144. Elsevier, Amsterdam (2005)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Verification, Model Checking, and Abstract Interpretation (VMCAI’04), LNCS, vol. 2937, pp. 44–57. Springer, Berlin (2004)
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from EAGLE to RULER. J. Logic Comput. (2008)
Bartetzko, D., Fischer, C., Moller, M., Wehrheim, H.: Jass-Java with Assertions. In: Runtime Verification (RV’01), ENTCS, vol. 55, pp. 103–117. Elsevier, Amsterdam (2001)
Blackburn, S.M., Garner, R., Hoffman, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M., Lee, H., Moss, J.E.B., Phansalkar, A., Stefanović, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’06), pp. 169–190. ACM, New York (2006)
Bodden, E.: J-LO, a tool for runtime-checking temporal assertions. Master’s thesis, RWTH Aachen University, Aachen (2005)
Bodden, E., Chen, F., Roşu, G.: Dependent advice: A general approach to optimizing history-based aspects. In: Aspect-Oriented Software Development (AOSD’09), pp. 3–14. ACM, New York (2009)
Bodden, E., Hendren, L., Lhoták, O.: A staged static program analysis to improve the performance of runtime monitoring. In: European Conference on Object-Oriented Programming (ECOOP’07), LNCS, vol. 4609, pp. 525–549. Springer, Berlin (2007)
Chaudhuri, S., Alur, R.: Instumenting C programs with nested word monitors. In: Model Checking Software (SPIN’07), LNCS, vol. 4595, pp. 279–283. Springer, Berlin (2007)
Chen, F., D’Amorim, M., Roşu, G.: A formal monitoring-based framework for software development and analysis. In: International Conference on Formal Engineering Methods (ICFEM’04), LNCS, vol. 3308, pp. 357–372. Springer, Berlin (2004)
Chen, F., Meredith, P., Jin, D., Roşu, G.: Efficient formalism-independent monitoring of parametric properties. In: Automated Software Engineering (ASE’09), pp. 383–394. IEEE, New York (2009)
Chen, F., Roşu, G.: Towards monitoring-oriented programming: A paradigm combining specification and implementation. In: Runtime Verification (RV’03), ENTCS, vol. 89, pp. 108–127. Elsevier, Amsterdam (2003)
Chen, F., Roşu, G.: MOP: An efficient and generic runtime verification framework. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’07), pp. 569–588. ACM, New York (2007)
Chen, F., Roşu, G.: Parametric trace slicing and monitoring. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS’09), LNCS, vol. 5505, pp. 246–261. Springer, Berlin (2009)
d’Amorim M., Havelund K.: Event-based runtime verification of Java programs. ACM SIGSOFT Softw. Eng. Notes 30(4), 1–7 (2005)
Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Model Checking and Software Verification (SPIN’00), LNCS, vol. 1885, pp. 323–330. Springer, Berlin (2000)
Eagle Technology. PCI 703 Series User’s Manual. http://www.eagledaq.com/display_product_36.htm
Eiffel Language. http://www.eiffel.com/
Goldsmith, S., O’Callahan, R., Aiken, A.: Relational queries over program traces. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’05), pp. 385–402. ACM, New York (2005)
Havelund, K., Nunez, M., Roşu, G., Wolff, B. (eds): Formal Approaches to Testing and Runtime Verification (FATES/RV’06), LNCS, vol. 4264. Springer, Berlin (2006)
Havelund, K., Roşu, G.: Monitoring Java programs with Java PathExplorer. In: Runtime Verification (RV’01), ENTCS, vol. 55, pp. 97–114. Elsevier, Amsterdam (2001)
Havelund, K., Roşu, G.: Monitoring Java programs with Java PathExplorer. In: Runtime Verification (RV’01), ENTCS, vol. 55, Elsevier, Amsterdam (2001)
Havelund, K., Roşu, G.: Monitoring programs using rewriting. In: Automated Software Engineering (ASE’01), pp. 135–143. IEEE, New York (2001)
Havelund, K., Roşu, G. (eds): Runtime Verification (RV’02), ENTCS, vol. 70. Elsevier, Amsterdam (2002)
Havelund, K., Roşu, G. (eds): Runtime Verification (RV’04), ENTCS, vol. 113. Elsevier, Amsterdam (2004)
Havelund, K., Roşu, G.: Synthesizing Monitors for Safety Properties. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), LNCS, vol. 2280, pp. 342–356. Springer, Berlin (2002)
Havelund K., Rosu G.: Efficient monitoring of safety properties. J. Softw. Tools Technol. Transf. 6(2), 158–173 (2004)
Hoare C.: Communicating Sequential Processes. Prentice-Hall Intl., New York (1985)
Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. Technical report (1971)
ISO/IEC 14977:1996, Information technology—syntactic metalanguage—Extended BNF. ISO, Geneva, Switzerland
JBoss. http://www.jboss.org
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: European Conference on Object-Oriented Programming (ECOOP’01), LNCS, vol. 2072, pp. 327–353. Springer, Berlin (2001)
Kiczales, G., Lamping, J., Menhdhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-oriented programming. In: European Conference on Object-Oriented Programming (ECOOP’97), LNCS, vol. 1241, pp. 220–242. Springer, Berlin (1997)
Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: Formally specified monitoring of temporal properties. In: Europoean Conference on Real-Time Systems (ECRTS’99) (1999)
Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’00), pp. 105–106. ACM, New York (2000)
Lu, H., Forin, A.: The design and implementation of P2V, an architecture for zero-overhead online verification of software programs. Technical Report MSR-TR-2007–99, Microsoft Research (2007)
Martin, M., Livshits, V.B., Lam, M.S.: Finding application errors and security flaws using PQL: a program query language. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’07), pp. 365–383. ACM, New York (2005)
Meredith, P., Jin, D., Chen, F., Roşu, G.: Efficient monitoring of parametric context-free patterns. In: Automated Software Engineering (ASE ’08), pp. 148–157. IEEE, New York (2008)
Meredith P., Jin D., Chen F., Roşu G.: Efficient monitoring of parametric context-free patterns. J. Autom. Softw. Eng. 17(2), 149–180 (2010)
Meyer B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, New Jersey (2000)
PCI SIG. Conventional PCI 3.0, PCI-X 2.0 and PCI-E 2.0 Specifications. http://www.pcisig.com
Pellizzoni, R., Buy, B.D., Caccamo, M., Sha, L.: Coscheduling of real-time tasks and PCI bus transactions. Technical report, University of Illinois at Urbana-Champaign. http://netfiles.uiuc.edu/rpelliz2/www/techreps/ (2008)
Pellizzoni, R., Meredith, P., Caccamo, M., Roşu, G.: Hardware runtime monitoring for dependable cots-based real-time embedded systems. In: Real-Time System Symposium (RTSS’08), pp. 481–491. IEEE, New York (2008)
Pellizzoni, R., Meredith, P., Nam, M.-Y., Sun, M., Caccamo, M., Sha, L.: Handling mixed-criticality in soc-based real-time embedded systems. In: Embedded Software (Emsoft’09), pp. 235–244 (2009)
Pnueli, A.: The temporal logic of programs. In Foundations of Computer Science (FOCS’77), pages 46–57. IEEE, New York (1977)
Roşu G., Havelund K.: Rewriting-based techniques for runtime verification. J. Autom. Softw Eng. 12(2), 151–197 (2004)
Roşu, G., Chen, F., Ball, T.: Synthesizing monitors for safety properties—this time with calls and returns. In: Runtime Verification (RV’08), LNCS, vol. 5289, pp. 51–68. Springer, Berlin (2008)
Sen, K., Roşu, G.: Generating optimal monitors for extended regular expressions. In: Runtime Verification (RV’03), ENTCS, vol. 89, pp. 162–181. Elsevier, Amsterdam (2003)
Sokolsky, O., Viswanathan, M. (eds): Runtime Verification (RV’03), ENTCS, vol. 89. Elsevier, Amsterdam (2003)
Soot website. http://www.sable.mcgill.ca/soot/
Thompson K.: Regular expression search algorithm. Commun. ACM 11(6), 419–422 (1968)
Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a Java optimization framework. In: IBM Centre for Advanced Studies Conference (CASCON’99), pp. 125–135. ACM, New York (1999)
Xilinx, Inc. Virtex-4 ML455 PCI/PCI-X Development Kit User Guide. http://www.xilinx.com/support/documentation/boards_and_kits/ug084.pdf
Author information
Authors and Affiliations
Corresponding author
Additional information
Supported in part by NSF grants CCF-0916893, CNS-0720512, and CCF-0448501, by NASA contract NNL08AA23C, and by a Samsung SAIT grant.
Rights and permissions
About this article
Cite this article
Meredith, P.O., Jin, D., Griffith, D. et al. An overview of the MOP runtime verification framework. Int J Softw Tools Technol Transfer 14, 249–289 (2012). https://doi.org/10.1007/s10009-011-0198-6
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-011-0198-6