Correct synchronization among activities is critical in a business process. Current workflow languages such as BPEL specify the control flow of processes explicitly. However, their procedural style may cause inflexibility and tangled code. We propose DSCL (Dag-acyclic-graph Synchronization Constraint Language) to achieve three desirable properties for a synchronization modeling language: declarative syntax, fine granularity and validation support. Instead of composing service out of structured constructs, DSCL declaratively describe the synchronization constraints in three basic relations on activity states. The state relationships collectively determine the execution order of activities in a composite process. The relationships are automatically translated into Petri Nets and simulated in the CPN/Tools, from which several correctness criteria can be validated for the composite process. We illustrate the advantages of DSCL with a Purchasing workflow example from BPEL 1.0 specification, and verify its correctness using CPN/Tools.