Z family on the Web with their UML Photos

 

Contents

*   Main approaches

*   XML Web browsing environment

*   XMI transformation environment

*   Conclusions

*   Acknowledgements

 

Main approaches

Motivation

One reason for the slow industrial take-up of formal methods (FM) is the lack of tools support and connections to the current industrial practice. Recent efforts and success in FM have been focused on building ‘heavy’ tools, such as theorem provers and model checkers. Although those tools are essential and important for applications of formal methods, in order to achieve wider acceptance, it's necessary to develop ‘light’ weight tools, such as easy-access browsers for formal specifications and projection/translation tools from formal specifications to industry popular graphical notations. World Wide Web (WWW) is a promising environment for software specification and design because it allows sharing design models and providing hyper-textual links among the models. Unified Modeling Language is commonly regarded as one of the dominating graphical notations for industrial software system modeling. It's important to develop links and tools from FM to WWW and to UML so that FM technology transfer can be successful.

 

Z is a state-oriented formal specification language based on set theory and predicate logic. Object-Z is an object-oriented extension to Z and has an active research community but lacks of tools support. TCOZ (Timed Communicating Object-Z) is a new formal specification language in the Z family, which combines the state-based formalism Object-Z with event-based formalism Timed CSP. Putting the “Z family” on the Web and taking their UML “photos” (ZML) are two main concerns of our work.

 

Furthermore, ZML can be used as an educational tool for helping students to understand:

 

Technical aspects

Our work uses the latest technology of eXtensible Markup Language (XML) and eXtensible Stylesheet Language (XSL) for displaying and transforming Z family notations on the web. In this demo, we firstly introduce the development of a web browsing environment and syntax checking facilities for Z, Object-Z and TCOZ languages using XML and XSL. (In the rest of the text, the term Object-Z is used instead of Z and Object-Z since Z is a subset of Object-Z). With the emergence of XML Metadata Interchange (XMI) as a standard, e.g. Rational Rose UML supports XMI input; it is also possible to build up a transformation link and projection tools from Object-Z web specifications to UML via XSLT technology. We will also illustrate the detailed transformation processes from our XML structure into UML XMI format.

The main process and techniques for developing Z family web environment and projection to UML are depictured by following Figure 1.

 

Figure 1: overall diagram

 

Team members

Supervisor :  Dr. DONG, Jin Song

Students :       LIU, Jing

SUN, Jing

WANG, Hai

 

Back to top

XML Web browsing Environment

Customized XML syntax definition

Firstly, we define a customized XML document for Object-Z according to its syntax definitions. This document is used for checking the syntax validity of the user input specifications. The World Wide Web Consortium (W3C) has provided two mechanisms for describing XML syntax structures: Document Type Definition (DTD) and XML Schema. The formal is originated from SGML Recommendation and used a total different syntax. XML Schema is a kind of XML file itself and is going to play the role of DTD in defining customized XML structure in the future. It is consistent with XML syntax and easy to write over DTD. We use XML Schema to define our XML structure syntax for Object-Z.

 

Part of the XML Schema (for defining an Object-Z operation and class schemas) is as follow.

 

<?xml version="1.0" encoding="UTF-8"?>
<Schema xmlns="urn:schemas-microsoft-com:xml-data" xmlns:dt="urn:schemas-microsoft-com:datatypes">
     

      <!-- some definition omitted -->
      <ElementType name="op" content="eltOnly" order="seq">
            <element type="name" minOccurs="1" maxOccurs="1"/>
            <element type="delta" minOccurs="0" maxOccurs="1"/>
            <element type="decl" minOccurs="0" maxOccurs="*"/>
            <element type="st" minOccurs="0" maxOccurs="1"/>
            <element type="predicate" minOccurs="0" maxOccurs="*"/>
            <AttributeType name="layout" dt:type="enumeration" dt:values="simpl calc" default="simpl"/>
            <attribute type="layout"/>
      </ElementType>
      <ElementType name="classdef" content="eltOnly">
            <element type="name" minOccurs="1" maxOccurs="1"/>
      <!-- some definition omitted -->
            <element type="inherit" minOccurs="0" maxOccurs="1"/>
      <!-- some definition omitted -->
            <element type="state" minOccurs="0" maxOccurs="1"/>
            <element type="init" minOccurs="0" maxOccurs="1"/>
            <element type="op" minOccurs="0" maxOccurs="*"/>
      <!-- some definition omitted -->
      </ElementType>
      <!-- some definition omitted -->
</Schema>

It states that the op tag is an element of classdef and consists of one name, a delta list, a number of declarations decl, an horizontal line st and some predicate definitions. An attribute layout is defined to distinguish between vertical layout schemas simpl and horizontal layout schemas calc.

 

A complete version of the XML Schema definition is available.

Remark: For the purpose of machine interchange, a more detailed Z/Object-Z/TCOZ XML syntax definition (fully-annotated XML Schema definition) is also available. A fully annotated BirthdayBook example in ZML (fully-annotated BirthdayBook example) is also available. A XML Schema definition for Z specification language in ISO standard is defined here.

 

Entity declarations

Z/Object-Z languages consist of a rich set of mathematical symbols. Those symbols can be presented directly in Unicode that is supported by XML. We have defined all the entities in the DTD so that users do not have to memorize all the Unicode numbers when authoring their XML documents. Part of the entity declaration DTD is defined as follows.

 

<?xml version="1.0" encoding="UTF-8"?>
<!-- some definition omitted -->

<!ENTITY emptyset "&#x2205;">
<!ENTITY mem "&#x2208;">
<!ENTITY nem "&#x2209;">
<!ENTITY pset "&#x2119;">
<!ENTITY fset "F">
<!ENTITY psetone "&#x2119;&#x2081;">
<!ENTITY fsetone "F&#x2081;">
<!ENTITY uni "&#x222a;">
<!-- some definition omitted -->

 

As most existing Z specifications were constructed in LaTeX, translating them to our format can be a trivial task due to that each entity is given a Z LaTeX compatible name. DTD is chosen to define our entity declaration because XML Schema does not support entity declaration at the moment.

 

A complete version of the entity DTD declaration and its symbol reference are also available.

 

Syntax usage

When authoring XML files, the user simply declares the name space of the XML schema and Entity DTD file as follows.

 

<?xml version="1.0" encoding="UTF-8"?>

<! --some definition omitted here -->

<!DOCTYPE unicode SYSTEM "http://nt-appn.comp.nus.edu.sg/fm/zml/unicode.dtd">

<objectZnotation xmlns="x-schema:

  http://nt-appn.comp.nus.edu.sg/fm/zml/objectZschema.xml"

  xmlns:HTML="http://www.w3.org/Profiles/XHTML-transitional">

<!-- some definition omitted -->

</objectZnotation>

 

With the above name space links, the XML editing tools can check the validity of the file via XML Schema definition and the DTD entity declarations. Any unspecified structures and entity symbols would be reported as a syntax error. The following is the Web browsing environment for the Light class (of the light control specification example) in our XML format.

 

<classdef layout="simpl" align="left">

<name>Light</name>

      <state>

            <decl>

                  <name>dim</name>

                  <dtype><type>Percent</type><type>&actuator;</type></dtype>

            </decl>

            <decl>

                  <name>on</name>

                  <dtype><type>&bool;</type></dtype>

            </decl>

      </state>

      <op layout="calc">

            <name>TurningOn</name>

            <predicate>dim := 100; on := true</predicate>

      </op>

      <op layout="calc">

            <name>TurningOff</name>

            <predicate>dim := 0; on := false</predicate>

      </op>

</classdef>

 

*  A complete version of the Light Control System specification in XML format is also available.

*  A complete version of the Birthday Book specification in XML format is also available.

 

Some remarks about the display of the XML specification demo:

*   Use IE5 for browsing, it supports XSL.

*   For the display of mathematical symbols, please install Unicode font (Arial Unicode MS, also provided in the Office 2000), after the installation make sure to set the Unicode font as your Web page font.

*   If the page could not be displayed properly (for some IE5, we encountered the same problem before), please update your IE5 to the new IE5.5 version.

*    If you have any problem or suggestion about the demo, please feel free to write to us.

XML – HTML transformation

With a valid XML file in hand, the next step is to transform the XML file into HTML format and display it on the web. XSL is a stylesheet language to describe rules for matching and transforming XML documents. An XSL file is also in XML format and it can perform the transformation between XML to HTML, XML to XML, XSL to XSL and so on. This kind of transformation can be done on the server side or the client side. Since Internet Explorer 5 (IE5) already supports XSL technology, this demo is based on client side (browser) transformation.  We have also developed a server side transformation environment for Netscape users via Active Server Page (ASP). A partial XSL stylesheet segment for displaying operation op and class definition classdef are defined as below.

 

<xsl:template match="op[@layout='simpl']">

<html>

  <tr>

    <!-- some definition omitted here -->

    <td height="24" valign="middle" align="left" nowrap="true">

      <i><xsl:value-of select="name"/></i>

      <!-- some definition omitted here -->

    </td>

    <!-- some definition omitted here -->

  </tr>

  <xsl:for-each select="delta | decl">

    <xsl:apply-templates select="."/>

  </xsl:for-each>

  <xsl:apply-templates select="st"/>

  <xsl:for-each select="predicate">

    <xsl:apply-templates select="."/>

  </xsl:for-each>

  <tr>

    <!-- some definition omitted here -->

  </tr>

</html>

</xsl:template>

 

<xsl:template match="classdef[@layout='simpl'] | classdef[@layout='gen']">

<html>

  <!-- some definition omitted here -->

  <a><xsl:attribute name="name"><xsl:value-of select="name"/></xsl:attribute></a>

  <!-- some definition omitted here -->

  <xsl:apply-templates select="tydef"/>

  <xsl:apply-templates select="state"/>

  <xsl:apply-templates select="init"/>

  <xsl:apply-templates select="op"/>

  <!-- some definition omitted here -->

</html>

</xsl:template>

 

XSL stylesheet file defines match method for each customized tag in the XML structure and describes the corresponding HTML codes. From the example above, in matching the "op" tag the XSL will display the operation name, delta list, declaration and predicates accordingly; in matching the "classdef" tag the XSL will first convert the class name into a HTML bookmark for the type reference usage and then apply the templates of drawing local type definition, state schema, initiation schema, operations and so on. To apply a template in XML is like to make a function call in programming, and each template will perform its own transformation. The users only need to write their XML files and add an URL to the defined XSL stylesheet location as below.

 

<?xml version="1.0" encoding="UTF-8"?>

<?xml-stylesheet type="text/xsl" href="http://nt-appn.comp.nus.edu.sg/fm/zml/objectzed.xsl"?>

 

With this link, the browser (IE5) will automatically transform XML document into desired HTML output. This process is totally user transparent.

 

A complete version of the XSL for transform XML to HTML is also available.

Browsing facilities

*   Type reference –- All user defined types and classes are treated as hyperlinks for type referencing purpose.

*   Schema expansions –- Inheritance relationship and schema calculus can be fully expanded to allow user to view the full aspect of the definition.

 

Back to top

XMI transformation environment

XMI in UML

For better understanding of the Object-Z/TCOZ models, we use UML to visualize them. As introduced earlier, the Object-Z/TCOZ models can be constructed in XML format. The textual specifications of UML models are in XMI format. Based on XSL Transformations (XSLT) technology, we define an XSL file to capture all translation rules from Object-Z/TCOZ (XML) to UML (XMI). XT is chosen as the XSLT processor and Rational Rose 2000 is used as the UML tool. By now we have fully implemented the visualization of static parts with UML class diagrams and are looking into the dynamic parts with UML state-charts. In our approach, all elements from the static view, such as attributes, operations, classes and their relationships (inheritance and aggregation) can be successfully captured through the transformation process.

 

The XML file for formal specifications and the XMI file for UML diagrams have similar structures.

An XMI file has the structure as follows.

 

<XMI xmi.version="1.0">

  <XMI.header>

  <XMI.content>

  <XMI.extensions>

</XMI>

 

The XMI.header section includes some optional information about UML model. Elements in UML diagrams, such as classes in class diagrams and states in the state-charts, are specified in the XMI.content section, while their positions, colors and other displaying properties are specified in the XMI.extensions section.

XML - XMI transformation

The XSL file used in this section is similar to the XSL file used in displaying Z specification in the previous section. The template technology plays a key role in implementing the translation rules.

Considering the implementation issues and the translation rules based on the formal model, the following guidelines are formed.

 

*   Each class in Object-Z XML models corresponds with a class in UML XMI models. They have the same name, attributes and operations.

*   If a type value in the Inherit part of a class matches the name of any other class in the current XML file, we regard that former class inherits the second one and illustrate the inheritance relationship between these two classes in the UML class diagram. In the case of spelling mistakes or missing reference of the $Inherit$ type, we ignore the relationship.

*   If a type value in the decl part, that is, the type of an attribute, matches the name of any class in current XML file, this is regarded as aggregation relationship between these two classes. The cardinality of the aggregation will be calculated and classified into UML aggregation ranges.

 

A complete version of the XML to XMI transformation demo is available.

 

Back to top

Conclusions

*      The first contribution of this work is the development of new techniques of using the latest technology of XML and XSL for displaying and browsing Z family languages on the web. Furthermore, extensible browsing facilities such as Z schema calculus and Object-Z/TCOZ inheritance expansions can be readily supported by our developed Z-XSL environment. Our ideas for putting Z family on the Web can be easily adopted by other formal methods, such as VDM/VDM++. In fact, since TCOZ includes most Timed CSP constructs, its web environment can be used for CSP/Timed-CSP specifications. Perhaps this may create a new culture for constructing formal specification on the web (XML) rather than in LaTeX. We hope it can be the starting point for developing a standard XML environment for all formal notations --- Formal specification Markup Language (FML).

 

*      The second contribution of this work is the investigation of the semantic links and web transformation environment (XSLT) between Object-Z/TCOZ (in XML) with UML diagrams (in XMI). Although we have some ideas on Object-Z/TCOZ behavior projections to state-charts, the development of the Web environment for systematic transformation from Object-Z/TCOZ to state-chart/collaboration diagrams remains a challenge. The engineering work for developing further techniques and putting these techniques into commercial case tools perhaps requires involvement from industry partners. We are currently in contact with various UML tools vendors.

 

Back to top

 

Acknowledgements

We would like to thank Dr. Ian Toyn for his useful suggestion and improvements on the Unicode definitions.

This work is supported by the research project:

*   Integrated Formal Methods (R-252-000-050-107)

*   Adding Formality to UML (R-252-000-076-112)

 

Back to top

 

Last revised: Friday, November 30, 2001.