MAPPING SCDL/BPEL TO ADA FOR FORMAL VERIFICATION OF THE BEHAVIORAL PROPERTIES OF SERVICE-COMPONENT ARCHITECTURE

The Service Component Definition Language (SCDL) and the Web Service Business Process ExecutionLanguage (WS-BPEL) are the standards de-facto used in the modeling and implementing of ServiceComponent Architecture (SCA). However, these powerful languages lack a formal foundation for thespecification and verification of the SCA properties. In this study, the use of Wright formal ADL and Adaprogramming language was proposed to check the behavioral properties of SCDL/WS-BPEL ServiceComponent architectures. To achieve this, the mapping of SCDL/WS-BPEL to the Wright formal ADL wassuggested in order to verify the standard behavioral consistency of the source description. As a secondstep, the target specification could be transformed into Ada to check the specific and dynamic behavioralproperties of the SCDL/WS-BPEL source architecture.