SPECIFICATION AND VERIFICATION OF WORKFLOW APPLICATIONS USING A COMBINATION OF UML ACTIVITY DIAGRAMS AND EVENT B

Ahlem Ben Younes, Leila Jemni Ben Ayed

2010

Abstract

This paper presents a transformation of UML activity diagrams (AD) into Event B for the specification and the verification of workflow applications. With this transformation, UML models could be verified by verifying derived event B models, automatically, using the B powerful support tools like B4free. The workflows is initially expressed graphically with UML AD and translated into Event B. The resulting model is then enriched with Invariants/Assertions describing functional properties of workflow models such as deadlock-inexistence. We present translation rules of UML AD into EventB, and we propose also a translation process of UML AD into EventB specifications based on the refinement technique of Event B to encode the hierarchical decomposition in UML AD. Also, we propose a solution to specify time in Event B, and by an example of workflow application, we illustrate the proposed technique.

Paper Citation

in Harvard Style

Ben Younes A. and Jemni Ben Ayed L. (2010). SPECIFICATION AND VERIFICATION OF WORKFLOW APPLICATIONS USING A COMBINATION OF UML ACTIVITY DIAGRAMS AND EVENT B . In Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT, ISBN 978-989-8425-23-2, pages 312-316. DOI: 10.5220/0003012003120316

in Bibtex Style

@conference{icsoft10,
author={Ahlem Ben Younes and Leila Jemni Ben Ayed},
title={SPECIFICATION AND VERIFICATION OF WORKFLOW APPLICATIONS USING A COMBINATION OF UML ACTIVITY DIAGRAMS AND EVENT B},
booktitle={Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT,},
year={2010},
pages={312-316},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0003012003120316},
isbn={978-989-8425-23-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT,
TI - SPECIFICATION AND VERIFICATION OF WORKFLOW APPLICATIONS USING A COMBINATION OF UML ACTIVITY DIAGRAMS AND EVENT B
SN - 978-989-8425-23-2
AU - Ben Younes A.
AU - Jemni Ben Ayed L.
PY - 2010
SP - 312
EP - 316
DO - 10.5220/0003012003120316