基于自动机理论的UML活动图模型检验方法

UML活动图被认为是最合适的软件过程描述语言,研究UML活动图的模型检验方法是很有必要的.提出一种基于自动机理论的UML活动图的模型检验方法.该方法给出UML活动图的形式语义,通过计算RTC-STEP,得到LTS,并将LTS映射到Büchi自动机,用LTL表示系统性质,并将LTL公式转换为相应的Büchi自动机,用基于自动机理论的模型检验方法检验UML活动图.