A Toolset for Supporting UML Static and Dynamic Model Checking

The Unified Modeling Language has become widely accepted as a standard in software development. Several tools have been produced to support UML model validation. However most of them support either static or dynamic model checking; and no tools support to check both static and dynamic aspects of a UML model. But a UML model should include the static and dynamic aspects of a software system. Furthermore, these UML tools translate a UML model into a validation language such as PROMELA. But they have some shortcomings: there is no proof of correctness (with respect to the UML semantics) for these tools. In order to overcome these shortcomings, we present a toolset which can validate both static and dynamic aspects of a model; and this toolset 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