A UML validation toolset based on abstract state machines

The Unified Modeling Language has become widely accepted as a standard in software development. Several tools have been produced to support UML model validation. These tools translate a UML model into a validation language such as PROMELA. However they have some shortcomings: there is no proof of correctness (with respect to the UML semantics) for these tools; and there is no tool that supports validation for both the static and dynamic aspects of a UML model. In order to overcome these shortcomings, we present a toolset which is based on the semantic model using abstract state machines. Since the toolset is derived from the semantic model, the toolset is correct with respect to the semantic model. In addition, this toolset can be used to validate both the static and dynamic aspects of a model.