Date Added: Dec 2011
To solve the consistency problems of UML Activity Diagram, the paper proposes a method of UML Activity Diagram formalizing and model checking based on Description Logic. It describes the static semantics of the Activity Diagram using an Ontology description language OWL DL by providing an algorithm which can transform the static semantics of Activity Diagram into the codes of OWL DL. The dynamic semantics of the Activity Diagram is described by DL-Safe rules. The model checking rules are defined, which enables model consistency checking by using a symbol system. Finally, a case study is presented to verify the feasibility of the method.