A TCOZ-based Formal Model of UML Use Case Diagrams

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.