KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Ordoni, Elaheh; Mülle, Jutta; Böhm, Klemens

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. ... mehr

Open Access Logo

Volltext §
DOI: 10.5445/IR/1000093998
Veröffentlicht am 26.04.2019
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 2019
Sprache Englisch
Identifikator ISSN: 2190-4782
KITopen-ID: 1000093998
Verlag KIT, Karlsruhe
Umfang 26 S.
Serie Karlsruhe Reports in Informatics ; 2019,4
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page