A Formal Approach for Ensuring a Correct Reconfigurable Composite Service,