| 基于通信序列进程的UML序列图形式化方法 |
| |
| 引用本文： | 邓建波,张立臣,邓惠敏,徐碧红.基于通信序列进程的UML序列图形式化方法[J].计算机应用,2010,30(10):2727-2729. |
| |
| 作者姓名： | 邓建波 张立臣 邓惠敏 徐碧红 |
| |
| 作者单位： | 1. 广东工业大学2. 广东工业大学计算机学院3. 吉首大学 |
| |
| 基金项目： | 国家自然科学基金资助项目 |
| |
| 摘 要： | UML2.0序列图是一种描述对象之间动态协作和事件发展时间关系的视图,但是UML序列图缺乏精确的形式化语义，所以不利于对其所描述的系统进行形式化验证。为此，根据UML2.0语义文档及组合碎片包概念，基于通信序列进程(CSP)给出了UML序列图的基本元素和消息迹的形式化定义及生成规则，实现了UML序列图的形式化，为UML序列图在描述系统准确性和有效性方面提供了形式化的检验方法。最后通过ATM实例说明UML序列图这一过程的正确性。
|
| 关 键 词： | UML2.0序列图 形式语义 组合碎片包 通信序列进程 |
| 收稿时间： | 2010-04-16 |
| 修稿时间： | 2010-06-19 |
Formal method for UML sequence diagrams based on communication sequential processes |
| |
| DENG Jian-bo,ZHANG Li-chen,DENG Hui-min,XU Bi-hong.Formal method for UML sequence diagrams based on communication sequential processes[J].journal of Computer Applications,2010,30(10):2727-2729. |
| |
| Authors: | DENG Jian-bo ZHANG Li-chen DENG Hui-min XU Bi-hong |
| |
| Abstract: | UML2.0 sequence diagram describes the dynamic collaboration and expresses the relation among the time of events. However, the lack of precise formal semantics is not conducive for the systems to be described in formal verification. To solve this problem, according to UML 2.0 semantic document and combination of fragment packets, the basic elements of UML sequence diagram, message trace definition and generation rules were given based on Communication Sequence Process (CSP). The accuracy and validity of formal method for UML sequence diagrams describing the system was provided. Finally an ATM example proves the validity of this process. |
| |
| Keywords: | UML2 0 sequence diagram formal semantics combined fragment packet Communicating Sequential Process (CSP) |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用》浏览原始摘要信息 |
|
点击此处可从《计算机应用》下载全文 |
