Towards a formal approach for the verification of SCA/BPEL software architectures
2017 8th International Conference on Information, Intelligence, Systems & Applications (IISA)(2017)
摘要
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.
更多查看译文
关键词
Verification,SCA,BPEL,Wright,CSP,Software Architecture,Model-Checker,FDR2
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络