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

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