Using UML activity diagrams and event B for distributed and parallel applications

被引：0
|
作者：
Ben Younes, Ahlem
Ben Ayed, Leila Jemni
机构：
来源：
COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL I, PROCEEDINGS | 2007年
关键词：
specification; formal verification; validation; UML; event B; distributed systems; parallel applications;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper presents a specification and verification technique for distributed and parallel applications using formal and semi-formal methods. The proposed technique uses UML and Event B. The design is initially expressed graphically with UML, then translated into Event B and verified using the B powerful support tools. In this paper, we focus on the translation of activity diagrams into Event B, in order to verify workflow properties of distributed and parallel applications with the B prover. We present translation rules of activity diagrams into Event A and relation between hierarchical decomposition of activities in UML activity diagrams and the refinement in Event B.
引用
收藏
页码：163 / 170
页数：8
相关论文
共 50 条
  • [1] SPECIFICATION AND VERIFICATION OF WORKFLOW APPLICATIONS USING A COMBINATION OF UML ACTIVITY DIAGRAMS AND EVENT B
    Ben Younes, Ahlem
    Ben Ayed, Leila Jemni
    [J]. ICSOFT 2010: PROCEEDINGS OF THE FIFTH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES, VOL 2, 2010, : 312 - 316
  • [2] From Graphical Model in UML Activity Diagrams to Formal Specification in Event B for Workflow Applications Modeling
    Ben Younes, Ahlem
    Ben Ayed, Leila Jemni
    [J]. PROCEEDINGS OF INTERNATIONAL SYMPOSIUM ON COMPUTER SCIENCE AND COMPUTATIONAL TECHNOLOGY (ISCSCT 2009), 2009, : 496 - 499
  • [3] Graphical Debugging of Distributed Applications Using UML Object Diagrams to Visualize the State of Distributed Applications at Runtime
    Koch, Andreas
    Zuendorf, Albert
    [J]. MODELSWARD 2015 PROCEEDINGS OF THE 3RD INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT, 2015, : 223 - 230
  • [4] 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
    Ben Ayed, Leila Jemni
    Hamdi, Najet
    Hlaoui, Yousra Bendaly
    [J]. ICSOFT 2010: PROCEEDINGS OF THE FIFTH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES, VOL 2, 2010, : 329 - 332
  • [5] Refinement Based Modeling of Workflow Applications using UML Activity Diagrams
    Ben Younes, Ahlem
    Hlaoui, Yousra Bendaly
    Ben Ayed, Leila Jemni
    Jlassi, Rahma
    [J]. 2013 IEEE 37TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSACW), 2013, : 187 - 192
  • [6] A Meta-Model Transformation from UML Activity Diagrams to Event-B Models
    Ben Younes, Ahlem
    Hlaoui, Yousra Bendaly
    Ben Ayed, Leila Jemni
    [J]. 2014 38TH ANNUAL IEEE INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSACW 2014), 2014, : 740 - 745
  • [7] 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
    [J]. 16TH INTERNATIONAL CONFERENCE ON INFORMATION INTEGRATION AND WEB-BASED APPLICATIONS & SERVICES (IIWAS 2014), 2014, : 479 - 483
  • [8] Enhancing UML Activity Diagrams using OCL
    Sunitha, E., V
    Samuel, Philip
    [J]. 2013 IEEE INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE AND COMPUTING RESEARCH (ICCIC), 2013, : 1 - 6
  • [9] Validation of UML static diagrams using B
    Truong, NT
    Souquières, J
    [J]. SERP '05: PROCEEDINGS OF THE 2005 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH AND PRACTICE, VOLS 1 AND 2, 2005, : 915 - 920
  • [10] Using UML State Diagrams for Modelling the Performance of Parallel Programs
    Ortega Arjona, Jorge
    [J]. COMPUTACION Y SISTEMAS, 2008, 11 (03): : 199 - 210
12345