FORMAL ANALYSIS OF UML 2.0 ACTIVITIES USING GRAPH TRANSFORMATION SYSTEMS

被引：0
作者：
Rafe, Vahid [1 ]
Rahmani, Adel T. [2 ]
Rafeh, Reza [1 ]
机构：
[1] Arak Univ, Dept Comp Engn, Arak, Iran
[2] Iran Univ Sci & Technol, Dept Comp Engn, Tehran, Iran
来源：
INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING | 2010年 / 20卷 / 05期
关键词：
Activity diagram; graph transformation; verification; dynamic semantics; AGG; MODEL CHECKING;
D O I：
10.1142/S0218194010004918
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Graph transformation is a general visual modeling language which is suitable for stating the dynamic semantics of the designed models formally. We present a highly understandable yet precise approach to formally define the behavioral semantics of UML 2.0 Activity diagrams by using graph transformation. In our approach we take into account control flow and data flow semantics. Our proposed semantics is based on token-like semantics and traverse-to-completion. The main advantage of our approach is automated formal verification and analysis of UML Activities. We use AGG to design Activities and we use our previous approach to model checking graph transformation system. Hereby, designers can verify and analyze designed Activity diagrams. Since workflow modeling is one of the main application areas of the Activities, we use our proposed semantics for modeling and verification of workflows to illustrate our approach.
引用
收藏
页码：679 / 694
页数：16
相关论文
共 27 条
  • [1] [Anonymous], ACM SIGSOFT SOFTW EN
  • [2] [Anonymous], 2000, Int. J. Softw. Tools for Technol. Transf. (STTT), DOI [10.1007/s100090050046, DOI 10.1007/S100090050046]
  • [3] [Anonymous], 2004, DAT SYS APP
  • [4] Baldan P, 2005, LECT NOTES COMPUT SC, V3267, P18
  • [5] Baresi L, 2002, LECT NOTES COMPUT SC, V2505, P402
  • [6] BARESI L, 2007, ENTCS, V213, P3
  • [7] BEYER M, 1992, AGG1 0 TUTORIALS
  • [8] Bock C., 2004, J OBJECT TECHNOL, V3, P27
  • [9] Bock C., 2003, J OBJECT TECHNOL, V2, P7
  • [10] BOLTON C, 2000, LNCS, V1939
123