Verifying Workflow Models with Data Values - a Case Study of SMR Spectrum Auctions

Industry takes a great interest in verification techniques to improve the reliability of process designs. Providing reliable design in application domains like spectrum auctions is crucial. Spectrum auction revenue is considered as one of the principal sources for governmental income. Hence, analyzing the auction design before applying it can ensure absence of undesirable results of an auction. Those results might even be bad, if they occur with a probability of just higher than zero. Current verification approaches are mainly devoted to verify control ows only, although data values play a significant role in real life applications. Thus, these approaches are not sufficient to support data-centered work ows as spectrum auctions. We address this issue by providing a new data-centered verification approach to analyze Simultaneous Multi-Round (SMR) auction design in BPMN format. We show how to enhance a BPMN model by including important information, namely data values used in the work ow, which the standard BPMN 2.0 does not support. An example of a data value in a SMR auction is the "auctioneer's revenue". To enable the verification of data-centered properties, we have developed a transformation of a data-value enhanced BPMN model to Petri Nets respecting the semantics of certain data value usages. ... mehrFor that, we support dynamic and correlated data values. By employing a model checker and defining data-centered properties in CTL formula, we verify SMR auction models to find undesirable executions for auctioneers. For example, we can precisely detect the worst values of three important measures in auctions: efficiency, revenue, and bidder's profit. With it, we can not only find the undesirable outcomes, but also provide a counter-example to help an auctioneer to improve the auction design.