10.3969/j.issn.1004-731X.2007.22.050
基于自动机理论的UML活动图模型检验方法
UML活动图被认为是最合适的软件过程描述语言,研究UML活动图的模型检验方法是很有必要的.提出一种基于自动机理论的UML活动图的模型检验方法.该方法给出UML活动图的形式语义,通过计算RTC-STEP,得到LTS,并将LTS映射到Büchi自动机,用LTL表示系统性质,并将LTL公式转换为相应的Büchi自动机,用基于自动机理论的模型检验方法检验UML活动图.
UML活动图、形式语义、模型检验、Büchi自动机
19
TP311.5(计算技术、计算机技术)
解放军总装备部预研项目413060103
2008-01-24(万方平台首次上网日期,不代表论文的发表时间)
共4页
5311-5314