UML顺序图的一种形式化描述方法  

A Formal Description of UML Sequence Diagram

作　　者：张姝[1] 张广泉[1] 

机构地区：[1]重庆师范大学数学与计算机科学学院,重庆400047

出　　处：《重庆师范大学学报（自然科学版）》2007年第3期42-45,共4页Journal of Chongqing Normal University:Natural Science

基　　金：重庆市自然科学基金(No.CSTC2006BB2259);重庆市教委科学技术研究项目(No.040803);中国科学院计算机科学国家重点实验室开放课题(No.SYSKF0303)

摘　　要：统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。The Unified Modeling Language （UML） is a eommon graphieal modeling language. It has beeome a de faeto standard in the analyzing and designing the object oriented system. However, the UML is not a formal language, its laek of rigor and formal semantics prevents it from further developing. Linear temporal logic is a formal description language of the dynamic semantics by of the concurrent or the reactive program. It suits for precisely representing the dynamic semantics of a model. This paper defines formal syntax of the sequenee diagram and gives a deseription of its semanties by using the linear temporal logic. Moreover, a property of the model is proved. It provides the foundation for the analysis and validation of the model.

关 键 词：UML顺序图 形式化语法 形式化语义 线性时序逻辑 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]