UML_AD2EventB: An Approach to Generating Event B Specification from UML Activity Diagrams for The Workflows Specification and Verification

被引：0
|
作者：
Ben Younes, Ahlem
Ben Ayed, Leila Jemni
机构：
来源：
2009 IEEE CONGRESS ON SERVICES (SERVICES-1 2009), VOLS 1 AND 2 | 2009年
关键词：
Specification; Formal verification; Validation; UML; Event B; workflow application;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper, we present a new approach to generating Event B specification from UML Activity Diagrams (AD). The goal of this work is to define a formal semantics of activity diagrams that is suitable for workflow modelling. The semantics should allow verification Of Junctional requirements using the B powerful support tools like B4free. In important characteristic of workflows is that the workflow systems are reactive systems. In this paper, we present a formal syntax and semantic for UML AD endowed with interactive aspects (send/receive event concepts), and we illustrate the proposed technique by an example of workflow application.
引用
收藏
页码：330 / 333
页数：4
相关论文
共 41 条
  • [31] From Sequence Diagrams to Event B: A Specification and Verification Approach of Flexible Workflow Applications of Cloud Services Based on Meta-model Transformation
    Hlaoui, Yousra Ben Daly
    Ben Younes, Ahlem
    Ben Ayed, Leila Jemni
    Fathalli, Manel
    [J]. 2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 2, 2017, : 187 - 192
  • [32] Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification
    Mouakher, Ines
    Dhaou, Fatma
    Attiogbe, J. Christian
    [J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2022, 37 (01) : 4 - 28
  • [33] Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification
    Inès Mouakher
    Fatma Dhaou
    J. Christian Attiogbé
    [J]. Journal of Computer Science and Technology, 2022, 37 : 4 - 28
  • [34] Generating Automatic Unit Tests of Java']JavaScript Code from UML Class and Activity Diagrams
    Malanowska, Agnieszka
    Malkiewicz-Blotniak, Adrianna
    [J]. ENASE: PROCEEDINGS OF THE 16TH INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING, 2021, : 189 - 196
  • [35] Generating Maude Specifications from UML Interaction Overview Diagrams: A Graph Transformation Based Approach
    Djaoui, Chafika
    Kerkouche, Elhillali
    Chaoui, Allaoua
    Khalfaoui, Khaled
    [J]. 2018 FIFTH INTERNATIONAL SYMPOSIUM ON INNOVATION IN INFORMATION AND COMMUNICATION TECHNOLOGY (ISIICT 2018), 2018, : 109 - 116
  • [36] From Formal Specification of Code Mobility to Design and Implementation: an UML-based Mobile Agent Approach
    Badica, Amelia
    Badica, Costin
    [J]. PROCEEDINGS OF THE 10TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING, 2009, : 297 - +
  • [37] UMLTGF: A tool for generating test cases from UML activity diagrams based on grey-box method
    Yuan, Jiesong
    Wang, Linzhang
    Li, Xuandong
    Zheng, Guoliang
    [J]. Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2006, 43 (01): : 46 - 53
  • [38] UML Activity Diagram To Event-B: A Model Transformation Approach Based on the Institution Theory
    Achouri, Amine
    Ben Ayed, Leila Jemni
    [J]. 2014 IEEE 15TH INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION (IRI), 2014, : 823 - 829
  • [39] An approach for the specification and the verification of multi-agent systems interaction protocols using AUML and Event B
    Ben Ayed, Leila Jemni
    Siala, Fatma
    [J]. MSVVEIS 2008: MODELLING, SIMULATION, VERIFICATION AND VALIDATION OF ENTERPRISE INFORMATION SYSTEMS, 2008, : 190 - 198
  • [40] Code Generation for UML 2 Activity Diagrams Towards a Comprehensive Model-Driven Development Approach
    Gessenharter, Dominik
    Rauscher, Martin
    [J]. MODELLING FOUNDATIONS AND APPLICATIONS, 2011, 6698 : 205 - 220
12345