Abstract: UML is a modeling language in general use for industrial software systems. However, its 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 diagrams and gives several transition rules for class diagrams and collaboration diagrams, which makes it possible to apply the formal reasoning mechanism of TCOZ to analyzing UML diagrams. A detailed case study of a school information system illustrates our method for modeling and analyzing UML diagrams.