On the Validation of Invariants at Runtime

• Autorzy: Kosiuczenko P.
• Języki publikacji: EN

Abstrakty

EN

The paradigm of contractual specification provides a transparent way of specifying object-oriented systems. In this paradigm, system consistency is specified using so-called invariants. Runtime validation of invariants is a complex problem. Existing validation methods require either exhausting validation of an invariant for all objects of the corresponding class or the use of restrictive type systems. In this paper a non-exhaustive method of invariant validation is proposed. It is proved that the method is sound and an implementation of this method is discussed. It is shown also how to extract context free languages corresponding to OCL-invariants.

Słowa kluczowe

EN

contracts; framing; invariant validation; OCL; optimization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 125, nr 2
• Strony: 183--222
• Opis fizyczny: Bibliogr. 43 poz., wykr.

Twórcy

autor

Kosiuczenko P.

• Institute of Information Systems, WAT, Warszawa, Poland

Bibliografia

• [1] Aho A., V., Ullman, J., D., Principles of Compiler Design. Series in Computer Science and Information Processing, Addison-Wesley, 1977.
• [2] Abramsky, S., Jung, A., Domain Theory, In Handbook of Logic in Computer Science, Vol. 3, Clarendon Press, 1994, pp. 1 - 168.
• [3] Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hhnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P., The KeY Tool. Software and System Modeling, Vol 4(1), 2005, pp. 32 - 54.
• [4] Akehurst, D., Howells, G., McDonald-Maier, K., Implementing Associations: UML 2.0 to Java 5, Software and System Modeling, Vol. 6, Springer, 2007, pp. 3 - 36.
• [5] Avila, C., Flores, G., Cheon, Y., A Library-Based Approach to Translating OCL Constraints to JML Assertions for Runtime Checking. Departmental Technical Reports (CS), University of Texas at El Paso, Paper Nr 71. http://digitalcommons.utep.edu/cs_techrep/71
• [6] Baar, T. et al. Tool Support for OCL and Related Formalisms Needs and Trends, In J., M., Bruel (ed): Satellite Events at the MoDELS 2005 Conference, LNCS, Vol. 3844, 2006.
• [7] Banerjee, A., Naumann D., A., Rosenberg, S., Regional Logic for Local Reasoning about Global Invariants, In Proceedings of the Twenty-second European Conference on Object-oriented Programming (ECOOP), LNCS, Vol. 5142, Springer, July 2008, pp. 387-411.
• [8] Barnett, M., DeLine, R., Fahndrich, Leino, K., R., M., Schulte, W., Verification of Object-Oriented Programs with Invariants. Journal of Object Technology, Vol. 3(6), 2004, pp. 27 - 56.
• [9] Briand, L., Dzidek, W., Labiche, Y., Using Aspect-Oriented Programming to Instrument OCL Contracts in Java, Technical Report SCE-04-03, Carleton University, 2004, 100 p.
• [10] Bidoit, M., Hennicker, R., Tort, F., Wirsing, M., Correct realizations of interface constraints with OCL. In France R., Rumpe B. eds: The UML - Beyond the Standard, Proc. 2nd Int. Conf, UML’99, LNCS 1723, Springer, 1999, pp. 399 - 415.
• [11] Cengarle, M., Knapp, A., OCL 1.4/1.5 vs. OCL 2.0 Expressions: Formal Semantics and Expressiveness. Softw. Syst. Model., 3(1), Springer, 2004, pp. 9 - 30.
• [12] Clavel, M., Egea, M., Garcya de Dios, M., OCL 1.4/1.5 vs. OCL 2.0 Expressions: Formal Semantics and Expressiveness. 8th International Workshop on OCL Concepts and Tools (OCL 2008) at MoDELS’08, Electronic Communications of the EASST, Vol. 15, 2008.
• [13] DOT, Dresdener OCL Toolkit, http://dresden-ocl.sourceforge.net/
• [14] Dzidek, W., Briand1, L., Labiche, Y., Lessons Learned from Developing a Dynamic OCL Constraint Enforcement Tool for Java, Best Papers of Satelite Workshops at the Models’05 conference, LNCS, Vol. 3844, Springer, 2006, pp. 9 - 19.
• [15] Gogolla, M., Richters, M., Use: A UML-based Specification Environment. http://www.db.informatik.uni- bremen.de/projects/USE/.
• [16] Goguen, J., Meseguer, J., Order sorted algebra. Theoretical Computer Science, Vol. 105(2), Elsevier, Amsterdam, 1992, pp. 167-215.
• [17] Gopinathan, M., Sriram, R., K,., Runtime Monitoring of Object Invariants with Guarantee. In. Martin Leucker ed., Runtime Verification, 8th International Workshop, RV’08, LNCS, Vol. 5289, Springer, 2008, pp. 158-172.
• [18] Hennicker, R., Baumeister, H., Knapp, A., Wirsing. M., Specifying Component Invariants with OCL. GI Jahrestagung 2001, pp. 600 - 607.
• [19] Hertz, M., Immerman, N., Moss, J., E., Framework for Analyzing Garbage Collection. Foundations of Information Technology in the Era of Network and Mobile Computing, In R. Baeza-Yates, U. Montanari, N.a Santoro eds., Foundations of Information Technology in the Era of Networking and Mobile Computing, IFIP 17, TCS 2002, Kluwer, pp. 230-242.
• [20] Hoare C., A., R., The Verifying Compiler, a Grand Challenge for Computing Research. In. T., Genssler et al., Modular Programming Languages 2003, LNCS, Vol. 2789, 2003, pp. 25 - 35.
• [21] Hoare C., A., R., An axiomatic basis for computer programming. Communications of the ACM, Vol. 12(10), 1969, pp. 576 - 585.
• [22] Hoare C., A., R., Proof of Correctness of Data Representations. Acta Informatica, Vol. 1(4), 1972, pp. 271 - 281.
• [23] Hopcroft, J., Motwani, R., Ullman, J., Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Second Edition, 2001.
• [24] Kassios, I., T., Dynamic frames: Support for framing, dependencies and sharing without restrictions, FM’06, LNCS, Vol. 4085, 2006, pp 268 - 283.
• [25] Kiczales et al. An Overview ofAspectJ, LNCS, Vol. 2072, Springer, 2001, pp. 327 - 355.
• [26] Kosiuczenko, P., Specification of Invariability in OCL. In O. Nierstrasz et al., ed., MoDELS’06, LNCS, Vol. 4199, Springer, 2006, pp. 676 - 691.
• [27] Kosiuczenko, P., View-Oriented Specification of Invariability in OCL Specifying Invariable System Parts and Views, Software and System Modeling, Springer, 2011, DOI: 10.1007/s10270-011-0215-y, to appear.
• [28] Kuhlmann, M., Gogolla, M., Analyzing Semantic Properties of OCL Operations by Uncovering Interopera- tional Relationships, Ocl4All: Modelling Systems with OCL, Workshop atMoDELS’07, Electronic Communications of the EASST, 2008.
• [29] Leavens, G., T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Muller, P., Kiniry, J., JML Reference Manual, Report 2007/02/07, Iowa State University, 2007.
• [30] Leino, R., Towards Reliable Modular Programs. Technical Report Nr. 00000234, California Institute of Technology, 1995.
• [31] Meyer, B., Applying design by contract, Computer, Vol. 25(10), IEEE Computer Society Press, 1992, pp. 40 -51.
• [32] Meyer, B., Object-Oriented Software Construction. Series in Computer Science, Prentice-Hall International, N.J., 1998.
• [33] Mezei, G., Levendovszky, T., Charaf, H., Restrictions For OCL Constraint Optimization Algorithms. Proceedings of the Sixth OCL Workshop OCL for (Meta-)Models in Multiple Application Domains, Electronic Communications of the EASST, Vol. 5, 2006.
• [34] Middelkoop, R., Huizing, C., Kuiper, R., Luit. E., J., Specification and Verification of Invariants by Exploiting Layers in OO Designs. Fundamenta Informaticae, Vol. 85(1-4), 2008, pp. 377 - 398.
• [35] Muller, P., Modular Specification and Verification of Object-Oriented Programs. LNCS, Vol. 2262, Springer, 2002.
• [36] Muller, P., Poetzsch-Heffter, A., Leavance, G., Modular Invariants for Layered Object-Structures. Science of Computer Programming, Vol. 62 (3), Elsevier, 2006, pp. 253 - 286.
• [37] O’Hearn, P., Yang, H., Reynolds, J., Separation and information hiding, In ACM Symposium on Principles of Programming Languages (POPL), 2004, pp. 268 - 280.
• [38] OMG, OCL 2.3 Specification, Version 2.3.1, formal/2012-01-01, 2012.
• [39] Patnaik, S., Immerman, N. Dyn-FO: A parallel dynamic complexity class. Proceedings of 13th ACM Symposium on Principles of Database Systems,Minneapolis, Minnesota, May 1994, pp. 210 - 221.
• [40] Smans, J., Jacobs, B., and Piessens, F., Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic, In. (Drossopoulou, S. ed.): Proc. of ECOOP, LNCS, Vol. 5653, Springer, pp. 148 - 172.
• [41] Van Der Straeten, R., Casanova, R., Stirred but not Shaken: Applying Constraints in Object-Oriented Systems Proc. of NetObjectDays, 2001, pp. 138 - 150.
• [42] Van Orman Quine, W., Mathematical Logic, Revised Edition, Harper & Row, 1962.
• [43] Warmer, J., Kleppe, A., Object Constraint Language: Getting Your Models Ready for MDA. Addison Wesley, 2003.