AN UML ACTIVITIES DIAGRAMS TRANSLATION INTO EVENT B SUPPORTING THE SPECIFICATION AND THE VERIFICATION OF WORKFLOW APPLICATION MODELS From UML Activities Diagrams to Event B

被引：0
|
作者：
Ben Ayed, Leila Jemni [1 ]
Hamdi, Najet [1 ]
Hlaoui, Yousra Bendaly [1 ]
机构：
[1] Res Unit Technol Informat & Commun UTIC ESSTT, 5,Ave Taha Hussein,PB 56, Tunis 1008, Tunisia
来源：
ICSOFT 2010: PROCEEDINGS OF THE FIFTH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES, VOL 2 | 2010年
关键词：
Specification; Verification; UML; Event B; Workflow applications;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This paper exposes the transformation of UML activity diagrams into Event B for the specification and the verification of parallel and distributed workflow applications. With this transformation, UML models could be verified by verifying derived event B models. The design is initially expressed graphically with UML and translated into Event B. The resulting model is then enriched with invariants describing dynamic properties such as deadlock freeness, livelock freeness and reachability. The approach uses activity diagrams meta-model.
引用
收藏
页码：329 / 332
页数：4
相关论文
共 24 条
  • [1] SPECIFICATION AND VERIFICATION OF WORKFLOW APPLICATIONS USING A COMBINATION OF UML ACTIVITY DIAGRAMS AND EVENT B
    Ben Younes, Ahlem
    Ben Ayed, Leila Jemni
    ICSOFT 2010: PROCEEDINGS OF THE FIFTH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES, VOL 2, 2010, : 312 - 316
  • [2] UML_AD2EventB: An Approach to Generating Event B Specification from UML Activity Diagrams for The Workflows Specification and Verification
    Ben Younes, Ahlem
    Ben Ayed, Leila Jemni
    2009 IEEE CONGRESS ON SERVICES (SERVICES-1 2009), VOLS 1 AND 2, 2009, : 330 - 333
  • [3] From Graphical Model in UML Activity Diagrams to Formal Specification in Event B for Workflow Applications Modeling
    Ben Younes, Ahlem
    Ben Ayed, Leila Jemni
    PROCEEDINGS OF INTERNATIONAL SYMPOSIUM ON COMPUTER SCIENCE AND COMPUTATIONAL TECHNOLOGY (ISCSCT 2009), 2009, : 496 - 499
  • [4] From a B specification to UML StateChart diagrams
    Hammad, A
    Tatibouët, B
    Voisinet, JC
    Wu, WP
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2495 : 511 - 522
  • [5] A Meta-Model Transformation from UML Activity Diagrams to Event-B Models
    Ben Younes, Ahlem
    Hlaoui, Yousra Bendaly
    Ben Ayed, Leila Jemni
    2014 38TH ANNUAL IEEE INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSACW 2014), 2014, : 740 - 745
  • [6] A Proof of the Correctness of a Transformation Approach from UML Activity Diagrams to Event-B Models
    Ben Younes, Ahlem
    Hlaoui, Yousra BenDaly
    Ben Ayed, Leila Jemni
    16TH INTERNATIONAL CONFERENCE ON INFORMATION INTEGRATION AND WEB-BASED APPLICATIONS & SERVICES (IIWAS 2014), 2014, : 479 - 483
  • [7] Using UML activity diagrams and event B for distributed and parallel applications
    Ben Younes, Ahlem
    Ben Ayed, Leila Jemni
    COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL I, PROCEEDINGS, 2007, : 163 - 170
  • [8] A method for the translation from UML into Event-B
    Sun Weixuan
    Zhang Hong
    Fu Yangzhen
    Feng Chao
    PROCEEDINGS OF 2016 IEEE 7TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS 2016), 2016, : 349 - 352
  • [9] From UML Diagrams to Simulink Models: a Precise and Verified Translation
    Costa, Andrei
    Cavalheiro, Simone
    Foss, Luciana
    Ribeiro, Leila
    30TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, VOLS I AND II, 2015, : 1547 - 1552
  • [10] Net verifier of discrete event system models expressed by UML activity diagrams
    Kowalski, Tomasz
    2006 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-6, PROCEEDINGS, 2006, : 3405 - 3410
123