Specifying and Verifying Cross-Organizational Business Models: An Agent-Oriented Approach

Cross-organizational business processes are routine in today´s economy. Of necessity, enterprises conduct their business in cooperation to create products and services for the marketplace. Thus business processes inherently involve autonomous partners with heterogeneous software designs and implementations. Therefore, it would be natural to model such processes via high-level abstractions that reflect the contractual relationships among the business partners. Yet, in today´s IT practice, cross-organizational processes are modeled at a low level of abstraction in terms of the control and data flow among the participants. This paper makes the following contributions. First, it proposes a simple, yet expressive, declarative way to specify business models at a high level based on the notion of commitments. Second, it shows how such a high-level model maps to a conventional operational model. Third, it provides a basis for verifying the correctness of the operational representations with respect to the declarative business model using existing temporal model checking tools. This paper validates the above claims using the well-known Quote To Cash business process, e.g., as supported by vendors such as SAP and applied in large enterprises. In this manner, this paper helps bridge the gap between high-level business models and their IT realizations.