Workflow technology has become a standard solution for managing increasingly complex business processes. Successful business process management depends on effective workflow modeling, which has been limited mainly to modeling the control and coordination of activities, i.e. the control flow perspective. However, given a workflow specification that is flawless from the control flow perspective, errors can still occur due to incorrect dataflow specification, which is referred to as dataflow anomalies.Currently, there are no sufficient formalisms for discovering and preventing dataflow anomalies in a workflow specification. Therefore, the goal of this dissertation is to develop formal methods for automatically detecting dataflow anomalies from a given workflow model and a rigorous approach for workflow design, which can help avoid dataflow anomalies during the design stage.In this dissertation, we first propose a formal approach for dataflow verification, which can detect dataflow anomalies such as missing data, redundant data, and potential data conflicts. In addition, we propose to use the dataflow matrix, a two-dimension table showing the operations each activity has on each data item, as a way to specify dataflow in workflows. We believe that our dataflow verification framework has added more analytical rigor to business process management by enabling systematic elimination of dataflow errors.We then propose a formal dependency-analysis-based approach for workflow design. A new concept called "activity relations" and a matrix-based analytical procedure are developed to enable the derivation of workflow models in a precise and rigorous manner. Moreover, we decouple the correctness issue from the efficiency issue as a way to reduce the complexity of workflow design and apply the concept of inline blocks to further simplify the procedure. These novel techniques make it easier to handle complex and unstructured workflow models, including overlapping patterns.In addition to proving the core theorems underlying the formal approaches and illustrating the validity of our approaches by applying them to real world cases, we provide detailed algorithms and system architectures as a roadmap for the implementation of dataflow verification and workflow design procedures.