Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Brucker, A.D.; Longuet, D.; Tuong, F.; Wolff, B. (2013)
Languages: English
Types: Book
\UML/ØCL is perceived as the de-facto standard for specifying object-oriented models in general and data models in particular. Since recently, all data types of \UML/ØCL comprise two different exception elements: \inlineoclinvalid (“bottom” in semantics terminology) and \inlineoclnull (for “non-existing element”). This has far-reaching consequences on both the logical and algebraic properties of ØCL expressions as well as the path expressions over object-oriented data structures, \ie, class models. In this paper, we present a formal semantics for object-oriented data models in which all data types and, thus, all class attributes and path expressions, support \inlineoclinvalid and \inlineoclnull. Based on this formal semantics, we present a set of ØCL test cases that can be used for evaluating the support of \inlineoclnull and \inlineoclinvalid in ØCL tools.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [1] P. B. Andrews. Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Kluwer Academic Publishers, 2nd edition, 2002. ISBN 1-402-00763- 9.
    • [2] M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), volume 3362 of LNCS, pages 49-69. Springer, May 25 2005. ISBN 978-3-540-24287-1. doi: 10.1007/b105030.
    • [3] A. D. Brucker and B. Wolff. An extensible encoding of object-oriented data models in HOL. Journal of Automated Reasoning, 41:219-249, 2008. ISSN 0168-7433. doi: 10.1007/s10817-008-9108-3. URL http://www.brucker.ch/bibliography/ abstract/brucker.ea-extensible-2008-b.
    • [4] A. D. Brucker and B. Wolff. HOL-OCL - A Formal Proof Environment for UML/OCL. In J. Fiadeiro and P. Inverardi, editors, Fundamental Approaches to Software Engineering (FASE08), number 4961 in LNCS, pages 97-100. Springer, 2008. doi: 10.1007/978-3-540-78743-3_8. URL http://www.brucker. ch/bibliography/abstract/brucker.ea-hol-ocl-2008.
    • [5] A. D. Brucker and B. Wolff. Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and Textual Modelling (OCL 2012), pages 19-24, 2012. ISBN 978-1-4503-1799-3. doi: 10. 1145/2428516.2428520. URL http://www.brucker.ch/bibliography/abstract/ brucker.ea-featherweight-2012.
    • [6] A. D. Brucker, M. P. Krieger, and B. Wolff. Extending OCL with null-references. In S. Gosh, editor, Models in Software Engineering, number 6002 in LNCS, pages 261-275. Springer, 2009. doi: 10.1007/978-3-642-12261-3_25. URL http://www. brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009. Selected best papers from all satellite events of the MoDELS 2009 conference.
    • [7] P. Chalin and F. Rioux. Non-null references by default in the Java modeling language. In SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems, page 9. ACM Press, 2005. ISBN 1- 59593-371-9. doi: 10.1145/1123058.1123068.
    • [8] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2):56-68, June 1940.
    • [9] G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. R. Cok, P. Müller, J. Kiniry, and P. Chalin. JML reference manual (revision 1.2), Feb. 2007. Available from http://www.jmlspecs.org.
    • [10] Object Management Group. UML 2.0 OCL specification, Apr. 2006. Available as OMG document formal/06-05-01.
    • [11] Object Management Group. UML 2.3.1 OCL specification, Feb. 2012. Available as OMG document formal/2012-01-01.
    • [12] M. Richters. A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universität Bremen, Logos Verlag, Berlin, BISS Monographs, No. 14, 2002.
  • No related research data.
  • No similar publications.

Share - Bookmark

Funded by projects


Cite this article