Behavioral Verification of Service Component Architecture

Currently,much research looks at treating the behavior properties beginning with the architectural design phase in SCA (Software Component Architectures) based applications. In this paper,we propose to map SCA onto the Wright ADL in order to verifythe behavioral consistency of SCA software architectures. To achieve this goal, we suggesttranslating this source software architecture into a Wright configuration. Using Wr2fdrtool, this Wright configuration can be automatically translated to a CSP specificationacceptable by the FDR2 model-checker.