Abstract
This paper addresses the problem of describing and analyzing data manipulation within business process workflow specifications. We apply a model-driven approach. We first augment typical workflow descriptions in Petri nets with ontologies written in the Web Ontology Language (OWL) and constraints written in Deontic Logic. Then we apply a model transformation from these augmented Petri nets to B machines, providing a full formal semantics of our models. A workflow, when represented as a Petri net with ontologies, can then be submitted to behavioural analysis with Petri net tools, and to analysis of data exchange with a B-based theorem prover.