Based On Z Formalization Of The Uml Use Case Diagrams

Unified Modelling Language has been a criterion of Object-Oriented Modelling Language and been used more and more widely. Formal software method can produce precise specification, and provide rigorous mathematical basis for software development. In order to make UML more precise, exhibit the advantage of formal method, and enhance the actual effect of formal method in software development, we put forward a new method that combine the formal method with Use Case Diagram of UML.This paper describes formally the Use Case Diagram with Z language, which provide formal basis for UML. Respectively we formalize the three components of Use Case Diagram: Actor, Use Case and System. Furthermore, The formal description of Use Case Diagram can be obtained by the combination of formalization of Actor, Use Case and System.