Service Composition is one of the pillars under Service Oriented Architecture. BPEL becomes the de-facto standard within this area. A key aspect when aggregating business processes using BPEL is to realize a compensation-based reliable service composition, often referred to as BPEL LRT(Long Running Transaction). But there lacks precise modeling on how to combine BPEL control flow with long running transactions. The paper presents a formal language named BPTX, which is a simplified version of BPEL at syntactic level and offers effective directions to underlying transaction coordinator as semantics. The paper also proposes an optimization not contained in traditional transaction processing: detect the failure destiny of a branch and react to it as early as possible.