Object Dynamics Formalization Using Object Flows within UML State Machines
DOI:
https://doi.org/10.18417/emisa.2.1.3Abstract
UML, the de-facto standard for object-oriented modeling, currently still lacks a rigorously defined semantics for its models. This makes formal analysis and verification of model properties extremely difficult. OCL, the Object Constraint Language is part of UML for the expression of system properties. To validate formally these properties, we first present a technique for transforming a UML object life cycle model into Object Petri nets. We are especially interested in the modeling of communicating systems and for this purpose we use the state machines as models of the object behaviour. Secondly, we resort to the object and sequence diagrams which provide respectively identified objects and events for initializing the Petri nets derived from the state machines. Thirdly, validation of OCL invariants which are translated into temporal logic properties to be checked on the Petri nets derived from the UML models, requires integration of object flows within the state machines. These object flows express the dynamic creation and deletion of objects in the class association ends. Our interest in the association ends is motivated by the fact that they constitute the most important constructs of OCL expressions. A case study is provided throughout the paper to illustrate the methodology.Downloads
Published
Issue
Section
License
Authors who publish with this journal agree to the following terms: Authors retain copyright and grant the journal 'Enterprise Modelling and Information Systems Architectures - International Journal of Conceptual Modeling' and the Gesellschaft für Informatik e.V. (GI) the permission of first publication, and the non-exclusive, irrevocable and non-time limited publication permission for the submitted work including the permissions to store, copy, distribute and reproduce their work in printed and electronic form for the duration of the legal copyright. This includes the right of translation. Authors grant the journal 'Enterprise Modelling and Information Systems Architectures - International Journal of Conceptual Modeling' and the Gesellschaft für Informatik e.V. (GI) the permission to license their work under a Creative Commons BY-SA 4.0 license that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book) given an acknowledgement of its initial publication in this journal.
Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access). The submitting corresponding author on behalf of all co-authors asserts that she/he is entitled to the granting of the above mentioned permissions for the submitted work.
