基于时序描述逻辑的UML顺序图形式化方法  

Formal Method of UML Sequence Diagram Based on Temporal Description Logic

作　　者：陈振庆[1] 

机构地区：[1]贺州学院计算机科学与工程系,广西贺州542800

出　　处：《计算机工程》2013年第3期36-40,共5页Computer Engineering

基　　金：广西壮族自治区教育厅基金资助项目(200911LX444);2010年度广西高等学校优秀人才资助计划基金资助项目

摘　　要：根据统一建模语言(UML)顺序图的时序特征,提出一种基于时序描述逻辑ALCQIUS的UML顺序图形式化方法。研究ALCQIUS时序扩展部分的语法和语义、ALCQIUS断言公式集一致性定理,给出ALCQIUS断言公式集一致性推理算法,并证明该推理算法的可判定性。以公安报警系统为例,说明基于ALCQIUS的UML顺序图形式化规约和形式化验证具备可行性,并且ALCQIUS为UML顺序图形式化提供了合理的逻辑基础。According to the temporal characteristic of Unified Modeling Language（UML） sequence diagram, this paper proposes a formal method of UML sequence diagram based on temporal description logic ALCQIus. The temporal expand syntax and semantics are given, the theorem of the assertion formulas of ALCQIus is studied, the consistency reasoning algorithms is put forward and its decidability is proved through the study of the assertion formulas of ALCQIus. Taking the public security alarm system as a example, the formal specification and formal checking of UML sequence diagram are explained through ALCQIus, and the ALCQIus provides more reasonable logic foundation for the formalization for UML sequence diagram.

关 键 词：时序描述逻辑 统一建模语言顺序图 静态语义 动态语义 形式化规约 形式化验证 

分 类 号：TP182[自动化与计算机技术—控制理论与控制工程]