| Correctness of business processes is becoming a critical issue of the day. The goal of the project is to develop methods for the verification of models of business processes. We choose to model business processes as workflows given by high-level Petri nets. We will pay special attention not only to the verification of the control flow, but to the verification of data properties as well. Our verification techniques will be based on the integration of structural analysis techniques specific for Petri nets with theorem proving and model checking. We will propose net transformations that will ease the application of verification techniques. The project team will make a prototype implementation for the developed techniques. The results will be evaluated on a set of case studies provided by practitioners. |