Web services are a relatively new paradigm for building distributed Web applications. Normally for proving properties of service compositions, and mapping the pre/post-conditions are assertions only on the initial and final states of the service respectively. They do not help in specifying and verifying ongoing behavior of a composite Web service system. We propose a formal framework for enriching composite service description with two additional assertions: assumption and commitment that facilitate compositional reasoning about services for the composition of their integration. The technique is based on Maude language, a rewriting logic based methodology in which formal modeling and analysis can be used from the earliest phases of system design to uncover many errors and inconsistencies, and to reach high assurance for critical components with runtime verification.