The way business processes are organised heavily influences the flexibility and the expenses of enterprises. The capability to address changing market needs in a timely manner and to provide appropriate pricing is indispensable in a world of internationalisation and growing competition. Optimising processes that cross enterprise boundaries potentially is a key success factor in achieving this goal but it requires the information systems of the participating enterprises to be consistently integrated. This gives rise to some challenging tasks. The personnel involved in building up business collaborations comes from different enterprises with different business vocabulary and background which requires extensive communication support. The lack of central technical infrastructure, typically prohibited by business politics, often calls for a distributed and computer-aided collaboration structure, so that the resulting complexity must be handled somehow. Nevertheless robustness is an important factor in building business collaborations as these may exchange goods of considerable value. This technical report proposes the use of a two step modelling approach that separates business logic, modelled in the so-called centralised perspective (CP), from its distributed implementation, modelled in the so-called distributed perspective (DP). The separation of these perspectives enables business people to concentrate on business issues and to solve communication problems in the CP whereas technical staff can concentrate on distribution issues. The use of stringent modelling rules is advised in order to provide the basis for formal analysis techniques as one means to achieve robustness. Considering the choreography of RosettaNet Partner Interface Processes (PIPs) as the subject of my analysis, UML activity diagrams for modelling the CP and WSBPEL for modelling the DP are described as enabling techniques for implementing the proposed two step modelling approach. Further, model checking is applied to validate the CP and DP models in order to detect errors in early design phases. As the adequacy of model checking tools highly depends on the detailed modelling techniques as well as the properties to be checked, a major part of our discussion covers relevant properties and requirements for a model checker.

Die Organisation von Geschäftsprozessen hat substantiellen Einfluss auf Flexibilität und Kosten eines Unternehmens. Die Fähigkeit, flexibel auf neue Marktanforderungen mit angemessenen Preisen reagieren zu können, ist in Zeiten der Internationalisierung und wachsenden Wettbewerbs überlebenswichtig. Die Optimierung unternehmensübergreifender Geschäftsprozesse ist ein potentieller Erfolgsfaktor für die Sicherstellung dieser Fähigkeit. Dazu müssen jedoch die Informationssysteme der beteiligten Unternehmen in konsistenter Weise integriert werden. So ergeben sich herausfordernde Aufgaben für Unternehmen. Typischerweise gehören Personen, die an der Realisierung einer Geschäftskollaboration mitwirken, unterschiedlichen Unternehmen an und haben ein unterschiedliches Verständnis von Geschäftsprozessen sowie unterschiedliches Vokabular zur Beschreibung von Geschäftsprozessen. Daher muss die Kommunikation zwischen diesen Personen besonders unterstützt werden. Weiterhin muss die Realisierung von Geschäftskollaborationen häufig verteilt vorgenommen werden, da keine zentrale technische Infrastruktur zur Verfügung steht oder aufgrund unternehmenspolitischer Restriktionen nicht möglich ist. Daher muss die entstehende Komplexität bewältigt werden. Schließlich werden im Rahmen einer Geschäftskollaboration häufig Güter beträchtlichen Werts ausgetauscht, sodass Robustheit eine maßgebende Anforderung an deren Realisierung ist. In diesem Arbeitsbericht wird ein zweistufiger Modellierungsansatz zur Bewältigung dieser Aufgaben vorgeschlagen, in dem die Modellierung von Geschäftslogik aus der so genannten "centralised perspective" (CP) von der Modellierung der verteilten Implementierung aus der so genannten "distributed perspective" (DP) getrennt wird. Durch die Trennung dieser Perspektiven können kaufmännische Experten Geschäftslogik aus der CP modellieren und Kommunikationsprobleme lösen wohingegen technische Experten die verteilte Implementierung aus der DP modellieren können. Weiter werden stringente Modellierungsregeln für die jeweilige Perspektive eingeführt, um die zu erstellenden Modelle formalen Analysetechniken zugänglich zu machen und so Robustheit als Ziel zu verwirklichen. Die in diesem Arbeitsbericht vorgestellte Fallstudie behandelt die Choreographie von RosettaNet Partner Interface Processes (PIPs). Für die Fallstudie werden als mögliche Technologien UML Aktivitätsdiagramme zur Modellierung aus der CP und WSBPEL zur Modellierung aus der DP eingesetzt. Zusätzlich werden Model-Checking-Tools (Model Checker) zur Validierung der Modelle in frühen Entwicklungsphasen eingesetzt. Da die Adäquatheit eines Model Checkers wesentlich von der Art des Eingabemodells und den zu validierenden Eigenschaften abhängt, ist ein wichtiger Teil dieses Berichts der Identifikation relevanter Modelleigenschaften und der Analyse der Anforderungen an einen Model Checker gewidmet.