摘要
统一建模语言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.
出处
《重庆师范大学学报（自然科学版）》
CAS
2007年第3期42-45,共4页
Journal of Chongqing Normal University:Natural Science
基金
重庆市自然科学基金(No.CSTC2006BB2259)
重庆市教委科学技术研究项目(No.040803)
中国科学院计算机科学国家重点实验室开放课题(No.SYSKF0303)
