loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2008 32nd Annual IEEE International Computer Software and Applications Conference
From UML Activity Diagrams to Event B for the Specification and the Verification of Workflow Applications
July 28-August 01
ISBN: 978-0-7695-3262-2
ASCII Text
x 
 
Ahlem Ben Younes, Leila Jemni Ben Ayed, "From UML Activity Diagrams to Event B for the Specification and the Verification of Workflow Applications," Computer Software and Applications Conference, Annual International, pp. 643-648, 2008 32nd Annual IEEE International Computer Software and Applications Conference, 2008.
 
 
BibTex
x
 
@article{ 10.1109/COMPSAC.2008.217,
author = {Ahlem Ben Younes and Leila Jemni Ben Ayed},
title = {From UML Activity Diagrams to Event B for the Specification and the Verification of Workflow Applications},
journal ={Computer Software and Applications Conference, Annual International},
volume = {0},
year = {2008},
issn = {0730-3157},
pages = {643-648},
doi = {http://doi.ieeecomputersociety.org/10.1109/COMPSAC.2008.217},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Software and Applications Conference, Annual International
TI - From UML Activity Diagrams to Event B for the Specification and the Verification of Workflow Applications
SN - 0730-3157
SP643
EP648
A1 - Ahlem Ben Younes,
A1 - Leila Jemni Ben Ayed,
PY - 2008
KW - Specification
KW - Formal verification
KW - UML AD
KW - Event B
KW - workflow applications
VL - 0
JA - Computer Software and Applications Conference, Annual International
ER -
 
This paper presents a new event-B based approach to reasoning about workflow applications. We show how an event-B model can be structured from UML Activity diagrams (UML AD) and then used to give a formal semantic to UML AD which supports proofs of their correctness. More precisely, we give rules for the translation of UML AD into event-B language. In particular, we propose a solution that uses the refinement in Event B to encode the hierarchical decomposition of activities in UML AD. The event-B method allows the definition of invariant describing required properties (deadlock-inexistence, liveness, fairness) and provides an automatic proof. We discuss the contributions and by an example of a workflow application, we illustrate the proposed approach.
Index Terms:
Specification, Formal verification, UML AD, Event B, workflow applications
Citation:
Ahlem Ben Younes, Leila Jemni Ben Ayed, "From UML Activity Diagrams to Event B for the Specification and the Verification of Workflow Applications," compsac, pp.643-648, 2008 32nd Annual IEEE International Computer Software and Applications Conference, 2008
Usage of this product signifies your acceptance of the Terms of Use.