Java-MOP: A Monitoring Oriented Programming Environment for Java

  • Feng Chen
  • Grigore Roşu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


A Java-based tool-supported software development and analysis framework is presented, where monitoring is a foundational principle. Expressive requirements specification formalisms can be included into the framework via logic plug-ins, allowing one to refer not only to the current state, but also to both past and future states.


Temporal Logic Regular Expression Logic Engine Runtime Check Monitoring Code 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with ltl in eagle. In: Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD 2004) (Satellite workshop of IPDPS 2004), Santa Fe, New Mexico, USA, April. IEEE Computer Society Press, Los Alamitos (2004)Google Scholar
  2. 2.
    Chen, F., D’Amorim, M., Roşu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 357–372. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Bartetzko, M.M.D., Fischer, C., Wehrheim, H.: Jass - java with assertions. In: Electronic Notes in Theoretical Computer Science, vol. 55. Elsevier, Amsterdam (2001)Google Scholar
  4. 4.
    Drusinsky, D.: Monitoring Temporal Rules Combined with Time Series. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 114–117. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Havelund, K., Roşu, G.: Workshops on Runtime Verification (RV 2001, RV 2002, RV 2004). ENTCS, vol. 55, 70(4). Elsevier, Amsterdam (2001–2002, 2004) (to appear)Google Scholar
  6. 6.
    Havelund, K., Roşu, G.: An overview of the runtime verification tool Java PathExplorer. Formal Methods in System Design 24(2), 189–215 (2004)zbMATHCrossRefGoogle Scholar
  7. 7.
    Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a Run-time Assurance Tool for Java. In: Proceedings of Runtime Verification (RV 2001). Electronic Notes in Theoretical Computer Science, vol. 55. Elsevier Science, Amsterdam (2001)Google Scholar
  8. 8.
    Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, pp. 105–106 (2000)Google Scholar
  9. 9.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)Google Scholar
  10. 10.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Upper Saddle River (2000)Google Scholar
  11. 11.
  12. 12.
    Sen, K., Roşu, G., Agha, G.: Runtime safety analysis of multithreaded programs. In: Proceedings of 4th joint European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003), ACM, New York (2003)Google Scholar
  13. 13.
    Sha, L., Rajkumar, R., Gagliardi, M.: The simplex architecture: An approach to build evolving industrial computing systems. In: Proceedings of The ISSAT Conference on Reliability (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Feng Chen
    • 1
  • Grigore Roşu
    • 1
  1. 1.Department of Computer ScienceUniversity of Illinois at Urbana – ChampaignUSA

Personalised recommendations