A MetaModel Approach for WorkFlow Modeling Based On Event B

We proposed a MetaModel approach in modeling and analysis of workflow based on event B. A workflow model is divided into three aspects: the promotion of process that we called step in operation, running time constraints and database updating. Basic properties such as activity dependency and time progressing are defined in a metamodel, a workflow model is a dynamic instance that written in event B and refined from metamodel and extends from every single static activities that written in normal B with data operations . We also provide an example to show how a workflow can be encoded into event B specification. The analysis of properties is up to the proof obligations that generated automatically from B tool kit.