Verification of Data-Value-Aware Processes and a Case Study on Spectrum Auctions

Verification techniques are fundamental to improve the reliability of process designs in practice. In application domains like auctions, the issue is extremely valuable; the goal of auction designers is to prevent undesirable executions and maximize certain outcome measures. Current verification approaches tend to be confined to control flows, even though data values play a significant role. We address this issue by proposing a new data-value-aware verification approach: We enhance process models with information on data values. Then we transform the data-value-aware process models to Petri Nets, respecting the semantics of data value usages. By employing an off-the-shelf model checker and specifying data-value centered properties, one can now verify data-value-aware process models. A distinctive feature of our approach is the specification of data values and of their modifications during the process. This enables the verification of interesting properties in many domains. We evaluate our approach against the use case of Simultaneous Multi-Round (SMR) spectrum auctions. We verify SMR auction models and compute extreme values of common auction measures such as revenue.