Premium
Formal verification approaches in the web service composition: A comprehensive analysis of the current challenges for future research
Author(s) -
Souri Alireza,
Rahmani Amir Masoud,
Jafari Navimipour Nima
Publication year - 2018
Publication title -
international journal of communication systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.344
H-Index - 49
eISSN - 1099-1131
pISSN - 1074-5351
DOI - 10.1002/dac.3808
Subject(s) - correctness , computer science , formal verification , model checking , service (business) , service composition , service discovery , software engineering , formal methods , web service , functional verification , world wide web , programming language , economy , economics
Summary Today, service composition is emerging paradigm on the communication networks such as cloud environments, internet of things, wireless sensor network, and software‐defined network. The goal of service composition method is to provide the interactions between user requirements and smart objects of intelligent communication systems. There have been many efforts to use formal verification and behavioral modeling methods to evaluate the service composition mechanisms. Up to now, there is not a comprehensive analysis research on this topic. Therefore, this paper focuses on several formal verification approaches that are performed to confirm the service composition correctness in communication networks. The objective of this paper is to comprehensively categorize and examine current research techniques on formal verification of the service composition. This research analysis provides an overview of recent service composition approaches according to structural and functional properties. Comparison results show that most of the verification approaches in explanation of the service composition correctness are semantic‐aware approach with 43%. The most used verification method for the service composition is model checking with 69%. The process algebra is used 29%, and some theorem proving methods are applied in 9% of the investigated mechanism. Moreover, most widely used modeling tools are NuSMV (22%), SPIN (17%), CPN (12%), UPPAAL (12%), Event‐B (10%), and PAT (5%).