An Automated Analysis of errors for BPM Processes modeled using an in-house Infosys tool

We chalk out a procedure for automatically analyzing BPM processes modeled using an in-house Infosys requirements modeling tool, called InFlux. By this analysis, we are able to check the processes for syntactical errors as well as errors due lack of soundness. In the first step of the analysis these processes are checked for syntactical errors using simple graph-search techniques. If these processes do not contain any such error, they are subjected to soundness analysis (i.e., checking for absence of deadlock and lack of synchronization) using two different approaches with the business process verification tool Woflan and the Petri net model checker LoLA. Depending on the existence of a cycle the models are either fed into Woflan or LoLA. We report our experience with the occurrence of errors in InFlux processes.