摘要： 根据统一建模语言(UML)顺序图的时序特征，提出一种基于时序描述逻辑ALCQIUS的UML顺序图形式化方法。研究ALCQIUS时序扩展部分的语法和语义、ALCQIUS断言公式集一致性定理，给出ALCQIUS断言公式集一致性推理算法，并证明该推理算法的可判定性。以公安报警系统为例，说明基于ALCQIUS的UML顺序图形式化规约和形式化验证具备可行性，并且ALCQIUS为UML顺序图形式化提供了合理的逻辑基础。
关键词:
时序描述逻辑,
统一建模语言顺序图,
静态语义,
动态语义,
形式化规约,
形式化验证
Abstract: 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.
Key words:
temporal description logic,
Unified Modeling Language(UML) sequence diagram,
static semantic,
dynamic semantic,
formal specification,
formal verification
中图分类号:
陈振庆. 基于时序描述逻辑的UML顺序图形式化方法[J]. 计算机工程, 2013, 39(3): 36-40.
CHEN Zhen-Qiang. Formal Method of UML Sequence Diagram Based on Temporal Description Logic[J]. Computer Engineering, 2013, 39(3): 36-40.