基于Promela的UML建模方法及其应用  

Promela-based UML Modeling Methods and Its Application

作　　者：舒良春[1] 饶俊[2] 肖美华[1] 尹传文[1] 

机构地区：[1]南昌大学计算中心,江西南昌330031 [2]江西省信息中心,江西南昌330046

出　　处：《计算机与现代化》2010年第2期101-104,共4页Computer and Modernization

基　　金：2008年江西省研究生创新专项资金省教育厅资助项目(YC08A032)

摘　　要：针对形式化方法与可视化方法的优缺点,本文提出形式化方法与可视化UML互补的建模方法,主要探讨用形式化方法验证UML模型,将UML模型转换为Promela模型,再用模型检测工具SPIN对Promela模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。In terms of the advantages and disadvantages of the formalization methods and file visualization methods, this paper pro- poses 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.

关 键 词：UML PROMELA SPIN 形式化方法 

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