Abstract
The UML Activity diagrams (ADs), are lack of formal semantics in UML official specifications and therefore they cannot be performed formal system behavior analysis. This paper firstly employs the Hoare's CSP (Communicating Sequential Processes) to formalize the behaviors of UML ADs and hence it can provide an approach to model checking UML ADs during software analysis or design stage since CSP is supported by model-checkers such as FDR.