A refinement-based approach for verifying dynamic changes on time-aware processes

Time is one of the main issues when dealing with process management. In fact, proper time handling can reduce cost and thus maximize profit for organizations. Then, modeling and verifying temporal constraints in business processes have become an area of intensive research. As a particular issue, the execution of these processes needs to be flexible by applying dynamic change operations to satisfy the variable organization requirements and to cope with unforeseen situations. Thus, it is crucial to re-ensure the temporal consistency of the changed processes. To do so, we propose a formal model which guarantees the correctness of time-aware processes while considering change operations. We used the Event-B method which supports an incremental development based on the refinement technique.