Abstract
A formal framework for software development and analysis is presented, which aims at reducing the gap between formal specification and implementation by integrating the two and allowing them together to form a system. It is called monitoring-oriented programming (MOP), since runtime monitoring is supported and encouraged as a fundamental principle. Monitors are automatically synthesized from formal specifications and integrated at appropriate places in the program, according to user-configurable attributes. Violations and/or validations of specifications can trigger user-defined code at any points in the program, in particular recovery code, outputting/sending messages, or raising exceptions. The major novelty of MOP is its generality w.r.t. logical formalisms: it allows users to insert their favorite or domain-specific specification formalisms via logic plug-in modules. A WWW repository has been created, allowing MOP users to download and upload logic plug-ins. An experimental prototype tool, called Java-MOP, is also discussed, which currently supports most but not all of the desired MOP features.
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.
References
Abercrombie, P., Karaorman, M.: jContractor: Bytecode Instrumentation Techniques for Implementing DBC in Java. In: ENTCS, vol. 70. Elsevier, Amsterdam (2002)
Aspectj project, http://eclipse.org/aspectj/
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-Based Runtime Verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)
Bartetzko, D., Fischer, C., Moller, M., Wehrheim, H.: Jass - Java with Assertions. In: ENTCS, vol. 55. Elsevier, Amsterdam (2001)
Chen, F., D’Amorim, M., Roşu, G.: Monitoring-Oriented Programming. Technical Report UIUCDCS-R-2004-2420, Univ. of Illinois Urbana-Champaign (2004)
Chen, F., Roşu, G.: Towards Monitoring-Oriented Programming: A paradigm combining specification and implementation. In: Workshop on Runtime Verification (RV 2003). ENTCS, vol. 89, pp. 106–125. Elsevier, Amsterdam (2003)
Cheon, Y., Leavens, G.T.: A Runtime Assertion Checker for JML. In: Software Engineering Research and Practice (SERP 2002). CSREA Press (2002)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)
Eclipse project, http://www.eclipse.org
Eiffel Software. The Eiffel Language, http://www.eiffel.com/
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for Java. In: PLDI 2002, pp. 234–245 (2002)
Gabbay, D.M.: The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 409–448. Springer, Heidelberg (1989)
Havelund, K., Roşu, G.: Workshops on Runtime Verification (RV 2001, RV 2002, RV 2004), to appear of ENTCS. vol. 55, 70(4). Elsevier, Amsterdam, 2001, 2002 (2004)
Havelund, K., Roşu, G.: Runtime verification. Formal Methods in System Design 24(2) (2004) (Special issue dedicated to RV 2001)
Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-Oriented Programming. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997)
Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a Runtime Assurance Tool for Java. In: Runtime Verification (RV 2001). ENTCS, vol. 55. Elsevier, Amsterdam (2001)
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 (2000)
Markey, N.: Temporal Logic with Past is Exponentially more Succinct. EATCS Bull 79, 122–128 (2003)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Upper Saddle River (2000)
Mop website, http://fsl.cs.uiuc.edu/mop
Pnueli, A.: The Temporal Logic of Programs. In: IEEE Symposium on Foundations of Computer Science, pp. 46–77 (1977)
Alur, R., Henzinger, T.A.: Real-Time Logics: Complexity and Expressiveness. In: IEEE Symposium on Logic in Computer Science, pp. 390–401. IEEE, Los Alamitos (1990)
Roşu, G., Havelund, K.: Rewriting-based Techniques for Runtime Verification. Automated Software Engineering (to appear, 2005)
Sen, K., Roşu, G.: Generating Optimal Monitors for Extended Regular Expressions. In: Workshop on Runtime Verification (RV 2003). ENTCS, vol. 89 (2003)
Sokolsky, O., Viswanathan, M.: Workshop on Runtime Verification (RV 2003). ENTCS, vol. 89. Elsevier, Amsterdam (2003)
Tarr, P.L., Ossher, H., Harrison, W.H., Sutton, S.M.: N Degrees of Separation: multi-dimensional separation of concerns. In: ICSE 1999, pp. 107–119 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, F., D’Amorim, M., Roşu, G. (2004). A Formal Monitoring-Based Framework for Software Development and Analysis. In: Davies, J., Schulte, W., Barnett, M. (eds) Formal Methods and Software Engineering. ICFEM 2004. Lecture Notes in Computer Science, vol 3308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30482-1_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-30482-1_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23841-6
Online ISBN: 978-3-540-30482-1
eBook Packages: Springer Book Archive