采用动态描述逻辑实现UML状态图特性检测

摘要：

状态图是UML(Unified Modeling Language)语言中刻画对象行为的重要视图,而如何对状态图模型定义的正确性和有效性进行检验一直是一个亟待解决的问题.本文提出采用动态描述逻辑(DFDR-AREDA)对UML状态图形式化,并利用该逻辑系统的推理能力对状态图相关静态和动态特性进行检测.我们首先将状态图描述为一个(DFDR-AFEDA)形式系统.其中,状态图中的一个状态对应于该形式系统中的一个状态,状态特性及描述被表示为该形式系统中的概念和公理,事件被表示为该形式系统中的动作.然后,我们通过(DFDR-AFEDA)概念测试来检验状态图状态可满足性和冗余性,通过公式可满足性测试来验证状态转移引起的对象特性变化.

关键词：UML、状态图、特性检测、动态描述逻辑

所属期刊栏目：34

分类号：TP3(计算技术、计算机技术)

资助基金：国家重点基础研究发展计划973计划2005CB321905

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

页数：共4页

页码：268-271