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

摘要：

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

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

所属期刊栏目：39

分类号：TP182(自动化基础理论)

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

在线出版日期：2013-11-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：36-40