Towards modelling and analyzing timed workflow systems with complex synchronizations

Nowadays, workflow systems are becoming very complex, involving time constraints, priorities on tasks as well as elaborated synchronization schemes. As a result, the specification and the verification of such systems are demanding much theory to prove their correctness and determine their qualitative and quantitative properties. In this paper, we mainly deal with complex synchronization on timed workflow systems. To address this issue, we redefine the concept of rendezvous as a mechanism to synchronize time constrained concurrent tasks of different privileges (Master, Slave). We discuss the different strategies that a rendezvous can follow, and hence we determine all the synchronizations patterns that could be considered in specifying its behaviour. From there, we deduce 36 generic synchronization rules that can be associated with the concept of rendezvous. Based on this theory, we extend the Time Petri Nets formalism to the concept of rendezvous to introduce the RTPN model (Time Petri Nets with rendezvous). Then, a subclass of RTPNs called Time Workflow-nets with Rendezvous (RTWF-nets), are defined for the modelling and the analysis of timed workflow systems. Finally, a case study is addressed to show how our framework can deal efficiently and elegantly with complex synchronization requirements.