Analyzing and Verifying UML State Diagrams with Object-Oriented Petri Nets

摘要：

Unified Modeling Language is the OMG standard modeling notation for object-oriented programming and has been widely applied to software and communication protocol development UML state diagram is important for dynamic description but it lacks of precise, formal semantics and limits the analysis and verification of the system. Object-oriented Petri Nets is a graphical modeling tool with strict formal semantics, specification and analysis methods. Based on the extended inhibitor arcs, the mapping rules of UML state diagrams to object-oriented Petri Nets are put forward. It provides a basis for the combination of UML with formal methods. Then the mapped UML state diagrams can be formally analyzed and verified. An example of IEEE 802.11 DCF is used to show the mapping and verifying processes.

关键词： UML state diagrams Object-oriented Petri Nets moping rules model analysis and verification IEEE802.11 DCF

作者: Tang Zhong Yang Xue

作者单位: School of Computer Science and Technology Shenyang University of Chemical Technology Shenyang,Liaoni School of Computer Science and Technology Shenyang University of Chemical Technology Shenyang, Liaon

会议类型: 国际会议

会议名称: 2010 Second Asia-Pacific Conference on Information Processing(2010年第二届亚太地区信息处理国际会议 APCIP 2010)

会议地点: 南昌

会议语种:英文

页码: 323-326

在线出版日期: 2010-09-17（万方平台首次上网日期，不代表论文的发表时间）