Workflow processes are represented as Petri nets with special entry and exit places and labeled transitions. The transition labels represent actions. We give a semantics for such nets in terms of transition systems. This allows us to describe and verify properties like {\em soundness}: preservation of the option to terminate successfully. We describe the composition of complex WF nets from simpler ones by means of operators: refinement, sequencing, choice, free merge, iteration, synchronous and asynchronous communication. These operators (except the communication operators) preserve soundness, giving correctness by design. A strategy for verification other properties is described.