Abstract: The state-chart of Unified Modeling Language(UML) is used to describe all the possible states and the transmisson conditions of states when the events occurre to analyze the system dynamically. This paper proposes refinement Calculus of Object Systems(rCOS) based on Unifying Theories of Programming(UTP) to specify the formal semantic of UML state-chart, which overcomes the limitation in the semantic research. And it provides the consistency checking with class diagram and sequence diagram, and gives the possibility of MDA development.

Key words: Unified Modeling Language(UML), refinement Calculus of Object Systems(rCOS), state-chart

摘要： 统一建模语言(UML)中的状态图用于描述类的对象所有可能的状态及事件发生时状态的转移条件，从而进行系统动态分析。针对现有关于UML状态图形式化语义研究中存在的不足，该文提出基于统一程序设计理论的对象精化演算系统，用于描述UML状态图的形式化语义，给出与类图、序列图的一致性检验，为模型驱动开发提供了可行性。

关键词: 统一建模语言, 对象精化演算系统, 状态图

CLC Number: 

• TP311