Abstract: UML's absence of formal semantics and rigorous reasoning mechanism results in its inaccuracy in system modeling and inefficiency for system development. TCOZ is a formal language combining features of Object-Z and Timed CSP, which is powerful in system modeling. Based on TCOZ, this paper proposes a formal model for UML Use Case diagram which provides not only a precise mathematical (description) for UML, but also a basis for its sound analysis and verification.