Paper Info
Title
CDLVT: A Formal Verification Tool of Non-functional Properties for WS-CDL Specification
Abstract
Service-oriented architectures (SOA) are hugely adopted. Within the SOA, service composition is fundamental. The design of composing service-based applications is mainly carried out throughout two composition techniques namely choreography and orchestration. Although these two composition models are different in nature, they are complementary. Choreography presents an abstract description of protocols. It offers a top view of the management rules which govern the interactions between the services involved in a decentralized application. On the other hand, orchestration provides details of the executable process at single peers which are necessary for the implementation of choreography. In this context, one open research problem, is the correct transformation of choreography specifications to orchestration specifications since orchestration provides more details to choreography specification. The choreography transformation has been the subject of several research works. Nevertheless, the existing works have considered that the choreography, on which their transformations are based, is correct by default. So, it is crucial to implement a checking process oriented to identify eventual incompatibilities that may arise. For this purpose, we present a formal verification approach based on the SPIN model-checker. The approach automatically transforms WS-CDL choreography specifications to Promela code for verification purposes. We verify non-functional properties that are expressed with linear temporal logic.
Year
DOI
Venue
2015
10.1109/WETICE.2015.14
WETICE Workshops
Keywords
Field
DocType
choreography,WS-CDL specification,formal verification
Open research,Non functional,Programming language,Computer science,Linear temporal logic,Choreography,Promela,Orchestration (computing),Formal verification,Executable
Conference
ISSN
Citations 
PageRank 
1524-4547
0
0.34
References 
Authors
11
5
Name
Order
Citations
PageRank
Sirine Rebai1101.28
Hatem Hadj Kacem24714.43
Mohamed Karaa310.68
Saúl E. Pomares Hernández422.41
Ahmed Hadj Kacem529564.22