We provide a formal semantics for timed DCR graphs with decision events and data, and show how the model supports merging declarative decision modelling and process modelling in one notation. We exemplify the model by an expense report process and discuss how decisions may be presented using DMN jointly with the DCR process notation. If data domains are bounded, models are finite state and allow formal verification of both safety and liveness properties. The formal model is fully implemented in commercial process design and workflow management systems provided by DCR Solutions and also freely available for academic use.