【摘要】 统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。更多还原

【Abstract】 The Unified Modeling Language(UML) is a common graphical modeling language.It has become a de facto standard in the analyzing and designing the object oriented system.However,the UML is not a formal language,its lack 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 sequence diagram and gives a description of its semantics 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.更多还原