Towards a formal approach for the verification of SCA/BPEL software architectures

Nowadays, a critical issue for complex Web systems development is the modeling and verification of its architectures. The standards SCA and BPEL are powerful complementary models for the development of complex Web service systems. In this paper, we proposed to map these models on the Wright/CSP ADL in order to verify the architectural properties of an SCA software architecture equipped with its BPEL behavioral aspects. The choice of this formal ADL is justified by the presence of the Wr2fdr tool that generates eleven standard properties related to the consistency of software architectures. In addition, using the Wr2fdr tool, this Wright/CSP target configuration was automatically translated to an FDR specification acceptable by the FDR2 model-checker.