How to use of the UML link.

It introduces the manner of operation of the UML link that is the function of VDMTools here.

Contents

VDMtools download and installation

Please download and install VDMTools(version 8.2 or later) from the download menu of VDM information web site(this website).

Tool options

The modeling tool used as a target and the file format of VDM++ generated from UML are selected as a tool option. A tool option is started by selecting "Project -> Tool Options" which is the menu item of VDM++ Toolbox, or pushing a button. A tool optional screen is shown in the following figures.

  • UML Interface : The modeling tool of target is selected.
  • New File Type : The file format of VDM++ generated from UML is selected.

Generating VDM from UML

The operating procedure which outputs a XMI file using JUDE Professional and Enterprise Architect is shown.

Output XMI file at JUDE Professional

The output of a XMI file selects "Tool -> XMI Input & Output -> Save as XMI Project" which is a menu item within JUDE Professional. The screen of the XMI project file output is shown in the following figures.

Since the screen which specifies a file name opens, a file name is specified and an "Save" button is pushed.

Output XMI file at Enterprise Architect

The package which outputs a XMI file is selected. In this example, since the class figure is stored in a "class" package, the "class" package has been selected.

Output of XMI file is menu item inside Enterprise Architect, "project -> reading and output -> the package XMI output" is selected.

On the screen which specifies a file name, a file name is specified and an "Save" button is pushed.

Convert XMI file to VDM++

Start UML Link

After starting VDMTools and creating a new project, an UML link function is started. The cooperation with a modeling tool is VDM++Toolbox. A window as shown in a figure starts by selecting "Window -> UML Link" which is a menu item inside, or pushing a button.

Since the screen which specifies the XMI file to input opens, the XMI file concerned is specified.

Convert UML to VDM++

Starting of an UML link will display a class list, as shown in a figure. When changing all the classes into VDM++, it checks that action of each class is "A", and a "Map" button is pushed.

The class specification child used here has a meaning of the following by "A" and "?."

  • "A" : This class was added by the processing in front of a model.
  • "?" : This class shows no recognition among models.

In the list, the button used for specification how to make two model forms cooperate, about each class is prepared.

  • From VDM++ to UML:
    • This operation carries out the map of the definition of the class defined by VDM++ to the same name class of UML. When this class has already existed in UML, this is updated, and a new class is generated when that is not right.
  • From UML to VDM++:
    • This operation carries out the map of the definition of the class defined by UML to the class of the same name of VDM++. When this class has already existed in VDM++, this is updated, and a new class is generated when that is not right.
  • Merge:
    • The definition of the class defined by VDM++ is merged to the definition of the class defined by UML by this operation.
  • Exclusion:
    • This operation excepts this class from the new model for processing. As for a result, this class is UML. It is removed from both a model and a VDM++ model.

Since the screen which specifies the preservation place of VDM++ to generate opens, the preservation place of a file is specified. Generated VDM++ is outputted in the form selected as the tool option.

Generateing UML from VDM++

The operation procedure which outputs a XMI file using VDMTools is shown.

Output XMI file at VDMTools

Start UML Link

After starting VDMTools and reading a project file, an UML link function is started.

Convert VDM++ to UML

Starting of an UML link will display a class list, as shown in a figure.

When changing all the classes into UML, it checks that action of each class is , and a "Map" button is pushed.

Generated XMI file

A success of conversion to an UML model will display Message "UML Model updated. Done." on a log window. The generated XMI file is placed by the same holder as the project file of VDM++.

Checking generated UML model

The operating procedure which checks an UML model using JUDE Professional and Enterprise Architect is shown.

Take in XMI file by JUDE Professional

Taking in of a XMI file selects "Tool -> XMI Input & Output -> Save as XMI Project" which is a menu item within JUDE Professional.

Since the screen which specifies an input file as shown in a figure opens, the XMI file concerned is selected.

The project title (here no_title) which is in a structure tree as shown in a figure is right-clicked, and it selects "Auto Create Detailed Class Diagram" of a sub menu.

As a result, as shown in a figure, a class figure is generated automatically.

Take in XMI file by Enterprise Architect

"File -> New project" which is a menu item within Enterprise Architect are selected.

Taking in of a XMI file selects "Project -> Read & Output -> Read XMI file" which are menu items within Enterprise Architect.

Since the screen which specifies an input file opens, the XMI file concerned is selected and "Read" button is pushed. The button "Close" if reading is completed is pushed.

The project title in a project browser (here no_title) is right-clicked, and "Add -> Add diagram" of a sub menu is selected.

Since a new diagram screen opens, a class figure is selected and the "OK" button is pushed.

The class below no_title to display is selected and it drops with class figure area. Then, since the attachment screen of an element opens, it selects "as a link" and the O.K. button is pushed.

"Diagram -> Auto layout diagram" is selected and a class figure is aligned.

Limitations

Relation with Type
The type definition of VDM is converted into the class in UML. Moreover, the record type is not converted into UML.
Notes concerning round-trip
When a class name is changed by UML, in VDM, the original class is deleted and it is interpreted as a new class having been added. As a result, the descriptive content of the original class will also be deleted.
How to write constraint, how in UML to appear
The constraints of Pre/Post have a description place in JUDE and each Enterprise Architect.
  • In Jude, it is indicated by "TaggedValue" in an operation property.
  • In EA, it is indicated to the "Pre/Post" tag in an operation property.
The notes to a function and operation with two or more return values
Since it cannot express by UML, two or more return values are not changed.
The invariant about an instance variable
The invariant of an instance variable are not changed into UML.
About the handling of the package in a class diagram
If a package is used for a class diagram, the class contained in a package will not cooperate in VDM. When using a package, we draw diagram where the class diagram which cooperates with VDM is another, or recommend you a package diagram.

Page top