Probabilistic Model Checking of Constraints in a Supply Chain Business Process

Business process models represent corporate activities, their dependencies and relations, as far as they are needed to reach a specific company goal. In practice, they often exhibit stochastic behavior, e.g., to deal with uncertain information. In this paper, we consider the problem of verifying properties over business processes that deal with such uncertain information. We employ a probabilistic model checking algorithm for verification, and demonstrate the applicability of this approach by a case study. Modeling and verification is achieved using the model checking tool PRISM. Based on the results, general specifications for modeling business processes using a probabilistic model checker are identified. Also, the difference between declarative and procedural business process modeling approaches is discussed. We propose to combine declarative and procedural techniques, thereby gaining increased expressiveness in modeling business processes, but still maintain verification feasible.