Current State
PhD student in the Faculty of Economics and Management of Sfax-Tunisia.
Teacher at the Faculty of Economics and Management of Sfax-Tunisia.
Member of the Research Unit on Development and Control of Distributed Applications
Education
Master degree, Computer Science, Faculty of Economics and Management of Sfax-Tunisia, 2011.
University Degree, Computer Science, Faculty of Economics Sciences and Management of Sfax-Tunisia, 2009.
Address
Department of Computer Science
Faculty of Economics and Management of Sfax (FSEGS).
University of Sfax.
Address: FSEGS, B.P. 1088, 3018 Sfax, Tunisia
Phone: (+216) 21 39 95 81
(+216) 55 39 95 81
Email : wael.sellami@gmail.com
Research activities
Research Topics
My main fields of interest are the composition of Web Services and verification with formal methods.
PhD Topics
My PhD thesis is supervised by Prof. Ahmed HADJ KACEM and Dr. Hatem HADJ KACEM.
My PhD research focuses on providing a rigorous approcah for dynamic composition of cloud services.
Master's thesis
My master project is supervised by Prof. Ahmed HADJ KACEM and Dr. Hatem HADJ KACEM.
My main field of interest is Modeling and verification fucntional and non-functional properties in web services composition. The aim of our work is to propose a methodology which aims to formally verify both of generic and specific properties of a composition modeled with BPEL 2.0.
Publications
[1] Wael SELLAMI, Hatem HADJ KACEM and Ahmed HADJ KACEM, BPELVT: A tool for formal validation of web service orchestrations. In In 21nd IEEE International Conference on Collaboration Technologies and Infrastructures (WETICE'2012), Toulouse, France June 25-27, 2012
[2] Hatem HADJ KACEM, Wael SELLAMI and Ahmed HADJ KACEM, A formal approach for the validation of web service orchestrations. In 21nd IEEE International Conference on Collaboration Technologies and Infrastructures (WETICE'2012), Toulouse, France June 25-27, 2012
Tools & Results
BPELVT: BPEL Verification Tool.
BPELVT is a formal approach of verifying non-functional properties for web services orchestrations. Two classes of properties have to be taken into account: generic and specific properties. Generic properties can be verified for any web service involved in a given orchestration. Specific properties are the dependent relations between activities for a given BPEL process. To do this, we have developed a tool which takes a web service orchestration specified with BPEL 2.0 as an input and a set of properties and returns the verification result as an output. The verification is achieved by using the SPIN model-checker. The transformation from BPEL to Promela, the input language for SPIN, is fullfilled with the use of ANTLR tool (Another Tool for Language Recognition).Educational activities
- 2011 - 2012: Faculty of Economics and Management of Sfax
- - IT and Internet Certificate (C2i)
- - Collaborative work

