ON V&V OF WEB SERVICE ORIENTED ARCHITECTURES
Abdelkader Dekdouk, Tarek Ahmed Helmy Amin Mohamed El-basuny · 2005
Now days it is widely accepted that the production of high quality software system requires a combination of techniques of testing (validation) and formal verification. These techniques have been widely applied in the development process of different kinds of software architectures. Recently service oriented architectures (SOA) have been emerged as a promising paradigm for supporting distributed computing. Different research contributions adopting the technique of testing have been carried out on SOA. However few works using formal verification have been done on SOA. In this paper we present our approach of formal verification to deal with this problem and situate it w.r.t. other contributions found in the literature treating this specific area. Our approach uses the technique of model-checking and simulation to verify the Web services interactions. For that, we use the modeling language BPEL4WS to describe the orchestration of the execution of Web services. Then we convert it to Promela, an input specification language of the Spin verifier tool in order to execute a series of ver ification and simulation procedures. All this is illustrated with a case study.