论文部分内容阅读
根据统一建模语言（UML）顺序图的时序特征，提出一种基于时序描述逻辑ALCQIus的UML顺序图形式化方法。研究ALCQIus时序扩展部分的语法和语义、ALCQIus断言公式集一致性定理，给出ALCQIus断言公式集一致性推理算法，并证明该推理算法的可判定性。以公安报警系统为例，说明基于ALCQIus的UML顺序图形式化规约和形式化验证具备可行性，并且ALCQIus为UML顺序图形式化提供了合理的逻辑基础。