uml2？0的形式化语义研究

由于uml2.0动态视图缺乏精确的语义，难以对它所表示的系统进行分析和验证。基于此，在描述uml2.0顺序图和状态图语法和语法约束的基础上，采用可执行的线性时序逻辑语言xyz/e定义其形式化语义，这样不仅便于uml2.0顺序图和状态图之间的模型转换，也为使用uml和形式化方法相结合描述软件体系结构的交互行为奠定了基础。