基于EMC和HA的UML Statecharts检测研究  

作　　者：王佳婧[1] 冯长宝[1] 佟鑫[1] 

机构地区：[1]吉林动画学院,吉林长春130012

出　　处：《通讯世界》2017年第16期282-283,共2页Telecom World

摘　　要：后续软件的正确开发取决于UML软件体系模型是不是反映了用户的需求。UML Statecharts可以把一个系统的行为正确地完整地描述出来,还可以展现系统功能。所以UMLstatecharts是UML模型检测的重要的对象。可以把UML Statecharts转成层次自动机HA[1],那么就可以让UML Statecharts没那么复杂,结构变得简单很多。之所以要在EMC[4]的基础上建立模型检测方法,是因为UML statecharts它有时序性。这种检测方法就是在对HA[1]描述的时候要使用Kripke[1]结构,对系统的性质进行描述时用时态逻辑,并标记状态。要判断出每一个状态能不能和相应的性质相匹配,对那些不符合的要给出不符合的状态序列,然后再次基础上优化。

关 键 词：UML STATECHARTS EMC[4] HA[1] Kripke[1 

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