Modular Verification of Inter-Enterprise Business Processes
In this paper, the authors propose to adapt the Symbolic Observation Graphs (SOG) based approach in order to abstract, to compose and to check Inter-Enterprise Business Processes (IEBP). Each component (local process) is represented by a SOG where only the collaboration actions of the process are visible while its local behavior and its private structure are hidden. The entire IEBP is then abstracted by the composition of the components' abstractions (i.e., their SOGs). The main result of this paper is to demonstrate that the composition of the SOGs is deadlock free if and only if the original IEBP is deadlock free. They implemented their adaptation of the SOG construction and compared their abstraction and modular verification approach with the Operating Guidelines technique.