The Study Of Formal Specification Based On UML

The specification phase is of great importance to the whole process of the software development, which is always considered as part of the requirement system. Using nature language as specification method has many advantages, for instance it can be easily understood and the communion between the customers and programmer become easy. But it can also brings in a lot of disadvantages, for example nature language brings in misconception and imprecision. Consequently it is important to develop a precise method which can be used as a means of software verification. Formal specification is precise method by giving a mathematical model which provides laws to refine and verify the software. A great numbers of methods of requirements analysis and specification have been put forward, which usually can be categorized into two classes: The formal methods and informal methods. Informal methods generally describe a software system through tables and graphs. UML, as one of the informal methods, is very popular and has been proved as a effective through the process of software development.This paper put forward a formal method of software specification and a set of mathematics models, which is based on UML and the program semantics of predicate transformer. With the advantage of both UML and formal specification, Application of the method in this paper can be easily expressed and understood together with the mathematic rigorism.