| 基于自动机理论的UML活动图模型检验方法 |
| |
| 引用本文： | 王聪,王智学.基于自动机理论的UML活动图模型检验方法[J].系统仿真学报,2007,19(22):5311-5314. |
| |
| 作者姓名： | 王聪 王智学 |
| |
| 作者单位： | 1. 解放军理工大学通信工程学院,江苏,南京,210007
2. 解放军理工大学指挥自动化学院,江苏,南京,210007 |
| |
| 基金项目： | 解放军总装备部预研项目 |
| |
| 摘 要： | UML活动图被认为是最合适的软件过程描述语言,研究UML活动图的模型检验方法是很有必要的。提出一种基于自动机理论的UML活动图的模型检验方法。该方法给出UML活动图的形式语义,通过计算RTC-STEP,得到LTS,并将LTS映射到Büchi自动机,用LTL表示系统性质,并将LTL公式转换为相应的Büchi自动机,用基于自动机理论的模型检验方法检验UML活动图。
|
| 关 键 词： | UML活动图 形式语义 模型检验 Büchi自动机 |
| 文章编号： | 1004-731X（2007）22-5311-04 |
| 修稿时间： | 2006年9月18日 |
Automaton Theory-based Model Checking Method for UML Activity Diagram |
| |
| WANG Cong,WANG Zhi-xue.Automaton Theory-based Model Checking Method for UML Activity Diagram[J].Journal of System Simulation,2007,19(22):5311-5314. |
| |
| Authors: | WANG Cong WANG Zhi-xue |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
