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

摘要

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