中文摘要：

基于UML模型的软件开发正在成为主流的软件开发方法，但是UML缺乏精确语义的缺陷阻碍了对模型进行精确分析。本文采用基于状态的方法给出了UML分析和设计模型的形式定义，在数据精化的框架内研究了模型的精化问题，并通过一个实例说明了如何寻找模型状态空间之间的变换关系。该方法是对UML模型进行分析和验证的基础，也是开发自动设计工具的理论依据。

英文摘要：

Aim. In our opinion, due to the nonexistence of recognized semantics for UML （Unifying Modeling Language） model elements, its full utilization has been severely limited. We now apply the Hoare and He＇s design calculus to giving precise definitions to UML model elements. In the full paper, we explain in detail bow to give precise definitions; in this abstract, we just add some pertinent remarks to listing the two topics of explanation. （1） design and design refinement and （2） UML model; under topic 1, we give definition 1 （design refinement）, definition 2 （data refinement）, and two criteria under definition 2 that must be both satisfied to ensure that the definitions of technical terms are precise; the subtopics of topic 2 are the requirements model of UML （subtopic 2. 1）, the design model of UML （subtopic 2. 2）, and model refinement （subtopic 2. 3）. Finally we give an example illustrating the application of our method on bow to give precise definitions to UML model elements. This example shows preliminarily that our method can formally analyze and verify the correctness of UML models, and furthermore develop semi-automatic computer-aided design tools.