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

Automaton Theory-based Model Checking Method for UML Activity Diagram

作　　者：王聪[1] 王智学[2] 

机构地区：[1]解放军理工大学通信工程学院,江苏南京210007 [2]解放军理工大学指挥自动化学院,江苏南京210007

出　　处：《系统仿真学报》2007年第22期5311-5314,共4页Journal of System Simulation

基　　金：总装备部十五预研项目(413060103)

摘　　要：UML活动图被认为是最合适的软件过程描述语言,研究UML活动图的模型检验方法是很有必要的。提出一种基于自动机理论的UML活动图的模型检验方法。该方法给出UML活动图的形式语义,通过计算RTC-STEP,得到LTS,并将LTS映射到Büchi自动机,用LTL表示系统性质,并将LTL公式转换为相应的Büchi自动机,用基于自动机理论的模型检验方法检验UML活动图。UML activity diagram is regarded as the most suitable language to describing the software process. It is worth to researching the approach of model checking UML activity diagram. An approach of model checking UML activity diagram was provided. The formal semantics of UML activity diagram was given. LTS （Labeled Transition System） was deduced by computing the RTC-STEP. And then the LTS could be mapped to a Bǖchi automaton. The system properties could be described by LTL. LTL formula could be translated to a Bǖchi automaton. UML activity diagram could be checked by automaton theory-based model checking method.

关 键 词：UML活动图 形式语义 模型检验 BÜCHI自动机 

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