In: 06: Bericht 267, Tagungsband des 13. Workshops Algorithmen und Werkzeuge für Petri-Netze, AWPN'06, FBI-HH-B-267, pages 47-53. September 06.
Abstract: Petri nets and in particular workflow nets as a process description language allow the application of formal verification methods, e.g., to prove soundness. Although tools for soundness checks do already exist, it is still difficult fo the workflow designer to correct the process model according to the output of these tests - mostly because diagnostic messages are not directly linked to the graphical model and intuition of the error source is missing. In this paper we propose an idea to overcome this problem. We present concepts to visualize verification output, in particular soundness violation messages in a more userfriendly way.