Premium
Formal modeling and verification of cloud‐based web service composition
Author(s) -
Raza Kazmi Syed Asad,
Qasim Awais,
Khalid Adnan,
Assad Ruttaba,
Shahbaz Muhammad
Publication year - 2020
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.5249
Subject(s) - computer science , web service , business process execution language , soundness , model checking , formal verification , web modeling , cloud computing , business process , software engineering , formal methods , service (business) , key (lock) , deadlock , formal specification , database , world wide web , distributed computing , computer security , operating system , programming language , engineering , economy , chemical engineering , compatibility (geochemistry) , economics
Summary Web service composition is a key technology to resolve cross‐organizational business process integration, and it faces many constraints and requirements as unexpected bugs can cause shutdown of the software. A high degree of reliability is expected from such systems, and formal modeling of web service composition is an active area of research. In this work, we propose a new approach for the formal modeling of diverse web service composition. Our approach verifies the terminate property on all possible runs of the system to ensure deadlock‐free workings. For a verification of the properties of interest, we use the NuSMV model checker and specify the properties in CTL*. The approach can be used to verify the soundness property of diverse web service composition to ensure live and deadlock‐free web services.