USING AToM3 FOR THE VERIFICATION OF WORKFLOW APPLICATIONS

Leila Jemni Ben Ayed, Ahlem Ben Younes, Amin Ben Brahim Achouri

2010

Abstract

In this paper, we propose an approach for the verification of workflow applications using AToM3 and Event B. Workflow carries applications where many actors take part and cooperate in order to execute operations. Upon composing those operations, many problems such as deadlock, freeness and livelock might appear. In this context, we are going to show how to build a meta-model for UML activity diagram in AToM3. From this meta-model, AToM3 generates a visual tool to build and to specify workflow applications where syntactical verification is made. Further, we are going to define a graph grammar to generate a textual code from the graphically specified workflow. This code will maintain information about all the activities and their dependencies. Another role of the graph grammar is to generate an Event B machine used for the verification of the workflow. Structural errors like deadlock and absence of synchronization can be captured from the resulted Event B model. Functional requirements are also verified using the resulted Event B model.

Paper Citation

in Harvard Style

Jemni Ben Ayed L., Ben Younes A. and Ben Brahim Achouri A. (2010). USING AToM3 FOR THE VERIFICATION OF WORKFLOW APPLICATIONS . In Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT, ISBN 978-989-8425-23-2, pages 32-39. DOI: 10.5220/0002930400320039

in Bibtex Style

@conference{icsoft10,
author={Leila Jemni Ben Ayed and Ahlem Ben Younes and Amin Ben Brahim Achouri},
title={USING AToM3 FOR THE VERIFICATION OF WORKFLOW APPLICATIONS},
booktitle={Proceedings of the 5th International Conference on Software and Data Technologies - Volume 2: ICSOFT,},
year={2010},
pages={32-39},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002930400320039},
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 - USING AToM3 FOR THE VERIFICATION OF WORKFLOW APPLICATIONS
SN - 978-989-8425-23-2
AU - Jemni Ben Ayed L.
AU - Ben Younes A.
AU - Ben Brahim Achouri A.
PY - 2010
SP - 32
EP - 39
DO - 10.5220/0002930400320039