摘要
根据统一建模语言(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.
出处
《计算机工程》
CAS
CSCD
2013年第3期36-40,共5页
Computer Engineering
基金
广西壮族自治区教育厅基金资助项目(200911LX444)
2010年度广西高等学校优秀人才资助计划基金资助项目
关键词
时序描述逻辑
统一建模语言顺序图
静态语义
动态语义
形式化规约
形式化验证
temporal description logic
Unified Modeling Language（UML） sequence diagram
static semantic
dynamic semantic
formal specification
formal verification
