UML活动图的模型检验方法UML活动图的模型检验方法

摘要

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