基于时序描述逻辑的UML状态图形式化验证  

Formal checking of UML statechart based on temporal description logics

作　　者：陈振庆[1] 

机构地区：[1]广西贺州学院计算机科学与工程系,贺州542800

出　　处：《制造业自动化》2012年第2期77-79,84,共4页Manufacturing Automation

基　　金：2010年度广西高等学校优秀人才资助计划项目:基于动态描述逻辑的UML状态图形式化方法

摘　　要：本文针对UML状态图具有动态行为和时序特征的特点,提出了一种新的描述逻辑,即时序描述逻辑TDDL(SHOIN(D))。首先给出了TDDL(SHOIN(D))的语法和语义,研究了TDDL(SHOIN(D))的断言公式集一致性推理和动作推理问题,给出了TDDL(SHOIN(D))的断言公式集一致性推理算法,并证明了该推理算法的可判定性;然后给出了动作包含、等价关系的判断方法,并证明了这些方法的可判定性。最后利用TDDL(SHOIN(D))对UML状态图进行了形式化验证。

关 键 词：时序描述逻辑 UML状态图 形式化规约 形式化验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]