PRODUS is a probabilistic data-aware business process modeling and verification framework. PRODUS uses a formal model to describe process behaviors as a labelled transitions system in which transitions are guarded by conditions defined over a probabilistic database and implements algorithms for testing probabilistic simulation preorder and of model checking in this context. In this paper, we demonstrate the use of PRODUS on a case study in the area of managing insurance premium.