| 基于Promela的UML建模方法及其应用 |
| |
| 引用本文： | 舒良春,饶俊,肖美华,尹传文. 基于Promela的UML建模方法及其应用[J]. 计算机与现代化, 2010, 0(2): 101-104. DOI: 10.3969/j.issn.1006-2475.2010.02.028 |
| |
| 作者姓名： | 舒良春 饶俊 肖美华 尹传文 |
| |
| 作者单位： | 1. 南昌大学计算中心,江西,南昌,330031
2. 江西省信息中心,江西,南昌,330046 |
| |
| 基金项目： | 2008年江西省研究生创新专项资金省教育厅资助项目(YC08A032) |
| |
| 摘 要： | 针对形式化方法与可视化方法的优缺点，本文提出形式化方法与可视化UML互补的建模方法，主要探讨用形式化方法验证UML模型，将UML模型转换为Promela模型，再用模型检测工具SPIN对Promela模型进行验证。最后通过实例对此转换方法进行验证，实验结果表明了此方法的有效性。
|
| 关 键 词： | UML Promela SPIN 形式化方法 |
Promela-based UML Modeling Methods and Its Application |
| |
| SHU Liang-chun,RAO Jun,XIAO Mei-hua,YIN Chuan-wen. Promela-based UML Modeling Methods and Its Application[J]. Computer and Modernization, 2010, 0(2): 101-104. DOI: 10.3969/j.issn.1006-2475.2010.02.028 |
| |
| Authors: | SHU Liang-chun RAO Jun XIAO Mei-hua YIN Chuan-wen |
| |
| Affiliation: | 1.Computing Center/a>;Nanchang University/a>;Nanchang 330031/a>;China/a>;2.Jiangxi Information Center/a>;Nanchang 330046/a>;China |
| |
| Abstract: | In terms of the advantages and disadvantages of the formalization methods and the visualization methods,this paper proposes modeling methods based on the two methods,which are reciprocal supplemented each other,it mainly focuses on how to use the formalization methods to verify the UML model,converts a UML model to a Promela specification,and then uses the famous model checking tool SPIN to verify it.And it is resulted to be available to verify the converting methods through an instance. |
| |
| Keywords: | UML Promela SPIN formalization |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
