A Validation Toolset for UML

Overview Method Functions Demo Download References Contact Information
Overview

Unified Modeling Language (UML) is becoming a standardized modeling notation for expressing object-oriented models and designs. The UML is based on an intuitive and easy to understand diagrammatic notation. More and more software developers are using UML to model their software in the early stages of software development. Recent research shows that software errors is most likely to be introduced during the requirement analysis and design stage; and these errors can have a lasting impact on the reliability, cost and safety of a system. Furthermore, requirement errors are between 10 and 100 times more costly to fix during later stages of the software lifecycle than during the requirements stage. Based on this result, we are building a UML toolset which can not only check a static aspect of a UML model but also verify some dynamic properties of a UML model.

Method
Our toolset is based on Abstract State Machines. As a formal method, it has been widely used in specification and verification for many software systems. Due to its successful application, we decide to build a UML toolset based on Abstract State Machines. The two parts of the ASMs are used in building this toolset. One is an ASM interpretor and the other is an ASM model checker. We use Xasm as our ASM interpretor to execute the ASM specification. For the ASM model checker, we translate the ASM specification into the SMV specification so as to implement model checking for a UML model. The following is an overall structure for the toolset.

overview

In addition, this toolset uses the XML Metadata Interchange Format (XMI) as its model input format. XMI is used to define an open information interchange model intended to give developers working with object technology the ability to exchange data in a standardized way. Therefore, it brings consistency and compatibility to applications created in collaborative environments. Many UML CASE tools provide a function to translate a UML model into XMI. In order to make this toolset support different UML CASE tools, we adopt XMI as an input format in this toolset for a UML model.
Functions

This toolset can do the following checking and validation:

  • syntax check: When a software developer develops a model for a system, (s)he gives a model for a real problem by presenting a set of UML diagrams. Because this tool supports the Object Constraint Language (OCL), this tool can be used to check whether a UML model is syntactically correct by comparing the model with the UML meta-model given by the OMG.
  • state check: When a software developer develops a model, (s)he has some reasonable states in his(her) mind. This toolset can be used to check whether these states are included in the model. In addition, this tool can also be used to check whether a model excludes some erroneous states.
  • dynamic property validation: This toolset can be used to check whether some dynamic properties are satisfied in a model. As a model is developed, more and more details about the model is added. One of the details about the model is its dynamic behavior. In UML, a developer can use dynamic diagrams in UML such as statechart diagram to describe a model's behavior. This toolset can validate some properties such as liveness property and safety property in UML dynamic diagrams.

Demo

There are several simple examples to show how this tool works.
Download

To be coming soon.
References
The following are some references about this toolset.

[1] K. Compton, Y. Gurevich, J. Huggins, W. Shen, An Automatic Verification Tool for UML, Technique Report CSE-TR-423-00, Dept. of EECS, The University of Michigan, May, 2000.
[2] K. Compton, J. Huggins, W. Shen, A Semantic Model for the State Machine in the Unified Modeling Language, Proceeding of Dynamic Behavior in UML Models: Semantic Questions, p.25-31, UML 2000 workshop, York, England, Oct. 2000.
[3] W. Shen, K. Compton, J. Huggins, A Validation Method for a UML Model Based on Abstract State Machines, In R. Moreno-Díacuteaz and A. Quesada-Arencibia, editors, Proceeding of EUROCAST 2001, pages 220-223, Canary Islands, Spain, Feb. 2001.
[4] W. Shen, K. Compton, J. Huggins, A Toolset for Supporting UML Static and Dynamic Model Checking, Proceeding of IEEE Automated Software Engineering 2001.
[5] W. Shen, K. Compton, J. Huggins, A Validation Tool for a UML Model Based on Abstract State Machines, In preparation.
Contact Information
Wuwei Shen
Software System Lab., Dept. of EECS
U of Michigan, 1301 Beal Ave.
Ann Arbor, MI 48109
Email: wwshen@eecs.umich.edu.