Formal specification to UML transformation demo

Please Note:

• This technique is based on the work of Web Display Formal Specification in ZML, which defined an XML format for writting formal specifications, it needs prerequisite understanding of this XML format.

• For correctly displaying the XML webpage including Z/Object-Z/TCOZ in your browser (Internet Explorer 5.5 only), You must have Unicode font to support those special formal notations. Please read the instructions in Light Control System Demo to get complete guide.

Introduction

This formal specification to UML transformation technique can be applied to Object-Z and Timed Communicating Object Z (an integrated formal techniques combining Object-Z and Timed-CSP).

The aim to transform formal models to a visual notation--- UML model. Currently, only transformation of the static views to class diagrams is implemented. The formal specification is written in XML (instead of the usual way---LaTeX), while with the emergence of XMI (XML Metadata Interchange), it becomes possible to build up an interchange of UML with other standards. The UML tool Rational Rose partially supports XML file Inport/Export. (To add this feature to your Rational Rose 2000, you have to download and install the Add-in built by Unisys Corporation.)

Therefore,XSLT technology is chosen to realize our tranformation rules, tranforming XML (formal model) to XMI (UML).

Formal model in TCOZ

In this demo, a TCOZ model for Light-Control system is used as an example. Because of the space limitation, in this page I only show you a small part of the specificaitons. To view the complete specification of the whole system, please click here.

		Light
		dim: Percent actuator
		on: ℬ
		TurningOn ≙ dim := 100; on := true
		TurningOff ≙ dim := 0; on := false

		ControlledLight
		Light
		button, dimmer: chan
		ButtonPushing ≙ button?1→([dim>0]∙ TurningOff ☐ [dim=0]∙ TurningOn )
		DimChange ≙ [n : Percent ]∙dimmer?n→([on]∙dim:=n ☐ [¬on]∙SKIP)
		MAIN ≙ μN ∙ ( ButtonPushing ☐ DimChange ); N

Click here to view XML source for the complete model of the light control system.

Transformation

• Using XSLT technique, I implement the translation rules (from TCOZ to UML) in an XSL file oz2uml.xsl. Since XSLT is currently not fully supported by any browser, I have to use James Clark's XT tool to transform the XML file into XMI file for UML diagram. For displaying Unicode, we generate XMI in HTML format. To try the tranformation process by yourself,
  1. please download the zip files(XT packaged as a Win32 executable and Light contorl model XML file and oz2uml.xsl)
  2. unzip them and save all files in one directory
  3. in DOS window, run the command " xt lighttcoz.xml oz2uml.xsl filename.html" (filename.html is the HTML view of the generated XMI file)
  4. copy the content(not source) of filename.html in your browser and save as XMIfile.xml. This is the ultimate XMI file you need for UML.

  Click here to view the generated XMI file for the example above.

• Import the XMI file into Rational Rose 2000 Enterprise, and you will get corresponding UML model. You can also directly download the XMI file ( lightXMI.xml ) for the complete system here and use Rose to test by yourself. Then you can manually adjust a bit for better layout.

  Here is the result of transformation to UML class diagram

• A reverse transformation from UML class diagram to Object-Z/TCOZ model is also available at XSL file for UML to Object-Z/TCOZ.