|
 
|
[RSB13] Modeling and formal verification framework of Web services composition
Conférence Internationale avec comité de lecture : International Conference on Control, Engineering & Information Technology (CEIT'13), Proceedings Engineering & Technology, June 2013, Vol. 2(2013), pp.140-145,Mots clés: Model checking, Web Services Composition, open workflow nets, NuSMV, CTL, soundness property.
Résumé:
Abstract: To ensure reliable and efficient communication in B2B environments, we relied on the use of composite Web services. Indeed, in some cases, a service cannot provide the functionality required by the user unless it communicates with other services. This leads to the notion of Web services composition. The communication of these Web services has to be guaranteed without errors such as deadlocks. In this way, formal verification of Web services composition is a focused-on research field. It is in this context that our work is proposed. We have developed a tool for modeling and formal verification of Web services composition which is based on the modeling of these services by open workflow nets: a special class of Petri nets used to model business processes which communicate together via interface places. This tool checks temporal properties written in CTL against a WSC model translated into SMV code. The verification is ensured by invoking the NuSMV Model Checker.
Equipe:
sys
Collaboration:
ENIT
BibTeX
| @inproceedings { | |||
| RSB13, | |||
| title | = | "{Modeling and formal verification framework of Web services composition}", | |
| author | = | " G. Rawand and Z. Sbaï and K. Barkaoui ", | |
| booktitle | = | "{International Conference on Control, Engineering & Information Technology (CEIT'13), Proceedings Engineering & Technology}", | |
| year | = | 2013, | |
| month | = | "June", | |
| volume | = | 2, | |
| issue | = | 2013, | |
| pages | = | "140-145", | |
| } | |||
