Interaction protocols as design abstractions for business processes

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

1

Interaction Protocols as Design Abstractions for Business Processes Nirmit Desai, Ashok U. Mallya, Amit K. Chopra, and Munindar P. Singh, Senior Member, IEEE

Abstract— Business process modeling and enactment are notoriously complex, especially in open settings where the business partners are autonomous, requirements must be continually finessed, and exceptions frequently arise because of real-world or organizational problems. Traditional approaches, which attempt to capture processes as monolithic flows, have proved inadequate in addressing these challenges. We propose business protocols among partners as components for developing business processes. A (business) protocol is an abstract, modular, and public specification of an interaction among different partner roles. Such protocols, when integrated with the internal business policies of the participants, yield concrete business processes. We show how this reusable, refinable, and evolvable abstraction simplifies business process design and development. We also show how business protocols are theoretically founded in the πcalculus. The protocols and their composition can be formalized which allows us to reason about the properties of the protocols. Index Terms— Multiagent systems, Software reuse, Interaction-Based modeling, Software design methodologies, rule-based processing, π-calculus

I. I NTRODUCTION

B

USINESS processes in open, Web-based settings typically involve complex interactions among autonomous, heterogeneous business partners. Conventionally, business processes are modeled as centralized flows, specifying exact steps for each participant. However, because of the exceptions and opportunities that arise in open environments, business relationships cannot be preconfigured to full detail. Flow-based models are inherently ill-suited to development and maintenance in the face of evolving requirements. Also, flows are not amenable to design abstractions such as reuse, refinement, and aggregation. Further, instead of treating all participants equally, conventional models classify the participants as clients and servers, thereby compromising the autonomy of the client participants. We propose multiagent systems as a model for business interactions. Agents mirror the autonomy and heterogeneity of real-world businesses and have rich interaction models. This paper describes a novel, agent-based approach for business process modeling and enactment. The key idea is to capture meaningful interactions as protocols. Protocols can involve multiple roles and address specific purposes such as ordering, payment, shipping, and so on. In order to be reusable, protocols emphasize the essence of the interactions and omit local details. Such abstract protocol specifications Authors are with the Department of Computer Science, North Carolina State University, Raleigh, NC 27695-7535, USA. E-mail: {nvdesai,aumallya,akchopra,singh}@ncsu.edu

are made publicly available as components and maybe reused by multiple enterprises. A key distinction between our approach and other works on protocols is that we give protocols a semantics in terms of the commitments among the roles of the protocol. Commitments help us capture the essence of the interactions supported by a protocol in a manner that is independent of specific sequences of messages exchanged among the participants. In simple terms, commitments provide a basis for modeling the state of the interaction, thus allowing a variety of possible executions depending on the specific circumstances of the parties involved. We conceptualize a business process as a cohesive set of protocols, to be enacted by agents representing real-world organizations. Whereas protocols specify the interaction from a global perspective, role skeletons specify the interaction from the perspective of a particular role. During enactment, each agent adopts a role in every protocol in which it participates, acquires the corresponding role skeletons, composes the skeletons, and integrates the resulting skeleton with its policies. A policy is a (typically private) description of an agent’s business logic that controls how it participates in a protocol. For example, a protocol may allow a role to choose among multiple actions; the agent playing that role would select an action based on its policy. Policies help determine the parameters of the messages being sent, typically based on the parameters of the messages previously received. On the practical side, our contributions include a language and tools for protocols called OWL-P. OWL-P describes concepts such as roles, the messages exchanged between the roles, and declarative protocol rules that describe the effects of sending messages in terms of commitments. It is captured as an ontology expressed in the Web Ontology Language (OWL) [19], which provides the primitives to specify particular protocols. Our software framework includes tools to facilitate specifying protocols in OWL-P, generating role skeletons from a protocol specification, and generating composites of multiple protocol specifications. During enactment, OWL-P specifications are compiled into Jess [10] rules, which then can be integrated with the local policies of the agents in a principled manner to yield concrete processes. We field such processes in the Java Agent Development Framework (JADE) [15]. On the theoretical side, we show how the π-calculus is a natural approach for formalizing certain aspects of protocols and policies. We show how to formally construct composite protocols and turn them into processes by integrating them with the policies. The formalization allows us to reason

2

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

about properties of the protocols such as kinds of protocol equivalences, correctness of the protocol composition process, and completeness of a composite protocol with respect to its component protocols. The key benefits of this approach are (1) a separation of concerns between protocols and policies in contrast to traditional monolithic approaches; (2) reusability of protocol specifications across business processes; (3) evolvability and refinability of processes by systematic composition of new protocols; and (4) flexibility of process enactment in a manner that respects local policies while adapting continually.

Rectangular nodes represent external interfaces through which a participant receives messages. Thus, the ordering of dark arrows, circles, and rectangles represents the local process of the participant. When there are multiple out-edges from a node, all of them are taken concurrently. The messages are labeled with numbers to indicate a possible order in which they might occur. For example, after message 9, the Merchant could send message 10 and message 13 in any order. Also, just one possible scenario is shown; an actual process specification might entail multiple scenarios.

A. Case Study

B. Shortcomings of Traditional Approaches The above process can be captured via a traditional flowbased approach such as BPEL [4]. Such a representation would be functionally correct, but inadequate from the perspectives of software engineering in open environments. The following are its shortcomings:

SHIPPER 14. status req 15. status resp

2. ship info

10. ship it

1. ship options

4. yes

3. feasible ?

M E R C H A N T

5. pay options

12. ship confirm#

8. Auth OK

7. auth req

16. captured

6. pay info 9. receipt 13. capture

C U S T O M E R

11. track#

17. delivery

PAYMENT GATEWAY Fig. 1.

A purchasing process

To effectively demonstrate and evaluate our methodology, we consider the case of a generic procurement process in an open market place. This commonly found business process involves multiple organizations namely, a Customer who wants to procure items, a Merchant who supplies items, a Shipper who is a logistics provider, and a Payment Gateway who authorizes payments. The payment-related interactions have been imported from the Secure Electronic Transactions (SET) standard [24]. Figure 1 depicts a simplified variant of such a process where items to be purchased have already been selected and the price has been agreed upon. Each participant is shown by a separate shaded region, the graph made of dark edges denotes the flow of the given participant. Circular nodes represent the participant’s internal business logic or policies, e.g., to decide the parameters of an outbound message.

Lack of Reusable Components The local processes of the partners are not reusable even though the patterns of interaction among the participants might be. Local processes are monolithic in nature, and formed by ad hoc intertwining of internal business logic and external interactions. Since business logic is proprietary, the local processes of one partner are not usable by another. For instance, if a new customer were to participate in this market, its local process would have to be developed from scratch. Lack of Semantics Traditional approaches expose lowlevel interfaces, e.g., via WSDL [31], but associate no semantics with the participants’ actions. This precludes flexible enactment (as needed to handle exceptions) as well as reliable compliance checking. Without semantics, we cannot determine if a deviation from a specific sequence of steps is significant. Inadequate Evolvability Suppose the merchant wishes to change the way it interacts with its customers, maybe because of new service features. Say the goods can be shipped before the payment is received. Due to an update in the merchant’s process, the customer agent may no longer be able to interact correctly. It is not clear what updates must be made in the process and where.

Organization Section II introduces some key concepts and terminology. Section III describes our protocol specification language and its semantics. Section IV discusses composite protocols and their construction and shows by an exception handling scenario, how protocol composition can be leveraged for refining protocols. Section V shows how augmenting policies with protocols can be used to develop processes. Section VI discusses the π-calculus formalization of our approach. Section VII compares our work with relevant research efforts and Section VIII concludes the paper with an outline of future directions.

DESAI et al.: INTERACTION PROTOCOLS AS DESIGN ABSTRACTIONS FOR BUSINESS PROCESSES

II. C ONCEPTS

AND

T ERMINOLOGY

Figure 2 shows our conceptual model for a treatment of business processes based on protocols and policies. Boxed rectangles are abstract entities (interfaces), which must be combined with business policies to yield concrete entities that can be fielded in a running system (rounded rectangles). Abstract entities can be published, shared, and reused among the process developers. They correspond to components in the Components-based software development (CBSD) [6] and to service specifications in service-oriented computing (SOC). We specify the protocol logic via rules that describe the interactions of the participating roles. Roles are abstract, and are adopted by agents to enable concrete computations. 1

Business Process

Abstract entity Concrete entity

1 aggregation of consults Implementation of

1

Local 1 Process 1

Business Logic

enacts 1

1

1 stipulates

2+

Agent

1

1 specified by 1

composedOf Fig. 2. policies

1

1+ 1+

Role couples

1 Business Protocol

1 Composite Skeleton

defines 1 1 Role Skeleton 2+

2+

1 Protocol Logic Composite Protocol

1+

1+

composition of

involves

1+

Implementation of

1

adopts

1+

2+

1 derives 1

derives

Conceptual model for business processes based on protocols and

Whereas the protocol logic specifies the protocol from the global perspective, a role skeleton specifies the protocol from the perspective of the corresponding participant role. That is, each role skeleton defines a role’s behavior in the given protocol. When an agent needs to participate in multiple protocols, it would adopt a role in each of them. A composite skeleton can be constructed by combining the adopted role skeletons according to some composition constraints. For example, in a supply chain process, a supplier would be a merchant when interacting with a retailer in a trading protocol and would be an item-sender in a shipping protocol for sending goods to the retailer. A composite skeleton for such a supplier could be

3

composed by combining role skeletons for a trading merchant and a shipping item-sender. The resultant composite skeleton could be published and reused for developing local processes of other suppliers. Alternatively, a composite protocol for supply chain can be composed from the requisite component protocols such as trading and shipping, and the role skeleton of the supplier can then be derived from the composite protocol. An agent’s private policies or business logic are described via rules. The local process of an agent is an executable realization of a composite skeleton obtained by integrating the protocol logic of the composite skeleton and the business logic of the agent. A business process is the aggregation of the local processes of all the agents participating in it. Conversely, a business process is an implementation of the constituent business protocols. A. Protocols and Commitments The concept of commitments has been proposed to capture a variety of contractual relationships, while allowing manipulations such as delegation and assignment, which are essential for open systems [25]. For example, a customer’s agreement to pay the price for the item after it is delivered is a commitment that the customer has towards the merchant. Violations of commitments can be detected; in some important circumstances, violators can be penalized. Such enforceability of contracts is necessary in practical settings where the participants are autonomous and heterogeneous [28]. Definition 1: A commitment C(x, y, p) denotes that agent x is responsible to agent y for bringing about condition p. Here x is called the debtor, y the creditor, and p the condition of the commitment. The condition can be expressed in a suitable formal language. Commitments can be conditional, denoted by CC(x, y, p, q), meaning that x is committed to y to bring about q if p holds where, q is called the precondition of the commitment. For example, the conditional commitment CC(c, b, goods(g), pay(p)) means that the customer c is committed to pay the bookstore b an amount p if the bookstore delivers the book g to the customer. When the bookstore delivers the goods, i.e., when the goods(g) proposition holds, the conditional commitment CC(c, b, goods(g), pay(p)) is automatically converted into the base-level commitment C(c, b, pay(p)). Commitments are created, satisfied, and transformed in certain ways. The following are the conventional operations defined on commitments [25]. 1) CREATE(x, c) establishes the commitment c in the system. This can only be performed by c’s debtor x. 2) CANCEL(x, c) cancels the commitment c. This can only be performed by c’s debtor x. Generally, cancellation is compensated for by making another commitment. 3) RELEASE(y, c) releases c’s debtor x from commitment c without c being fulfilled. This only can be performed by the creditor y. 4) ASSIGN(y, z, c) replaces y with z as c’s creditor. 5) DELEGATE(x, z, c) replaces x with z as the c’s debtor. 6) DISCHARGE(x, c) c’s debtor x fulfills the commitment. A commitment is said to be active if it has been created, but not yet discharged. The transformations of commitments are given as:

4

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

C(x,y,p)∧p discharge(x,C(x,y,p)) CC(x,y,p,q)∧p create(x,C(x,y,q))∧discharge(x,CC(x,y,p,q)) CC(x,y,p,q)∧q discharge(x,CC(x,y,p,q))

1) 2) 3)

(2)(8)proposition / commitment Rule Base

ExternalSlot

NativeSlot hasParameter

1

Commitment

represents

Message

1

1 hasSender

hasCreditor hasDebtor

Fig. 3.

Proposition 1

Rule

* involvesMessage

* dictates

hasReceiver 1

1

1 1

1

*

*

1 1

hasSlot

Slot

1

1

*

1 1

Protocol

contains

Knowledge Base

1

1

Role

consults

hasRole 2..*

(5)policy

(3)activate (4)invoke

Business Logic (Human Inputs)

To and from other participants Messages

OWL-P is an ontology for specifying protocols; it functions as a schema or language for protocols. OWL-P is formalized using OWL, so that the associated language has a clear conceptual basis, and tools such as Prot´eg´e [21] can be adapted for specifying protocols. The main computational aspects of protocols are specified using rules. We employ the Semantic Web Rule Language (SWRL) [12] for defining rules. SWRL allows us to specify implication rules (similar to horn rules in Prolog) over entities defined as OWL-P instances.

1

Policy Rules

Knowledge Base

Messaging Interface

A. OWL-P: OWL for Protocols

modifies

(7)mes s age

(1)mes s age

III. P ROTOCOL S PECIFICATION A business protocol is a specification of the allowed interactions among two or more participant roles. The specification focuses on the interactions and their semantics. What does it mean to send a certain message to a business partner? What is expected of the participants wishing to comply to a business protocol? How are the protocols specified? These are the questions we address in this section.

*

(6)activate

Protocol Rules

1

Basic OWL-P ontology

Figure 3 shows important OWL-P elements (nodes) and their properties (edges). The side of an edge with a little rectangle represents the domain of the corresponding property and the other side its range. Many of the properties are selfexplanatory and reflect the conceptual model introduced in Section II. A Message has a sender and a receiver, and can have several Slots as its parameters. We provide operational semantics for messages in terms of their effects on the commitments. For example, a message may create, discharge, delegate, assign, or cancel a commitment. Thus, messages can be thought of as operators over commitments. Slots are analogous to data variables. A slot is said to be defined when it is assigned a value and it said to be used when its value is assigned to another slot. A slot in a protocol may be assigned a value produced by another protocol and hence be represented as an External Slot. An external slot is untyped until it is given the

Fig. 4.

Local domain Public domain

Agent architecture: protocol and policy interplay

type of the external value to which it is bound. By contrast, a Native Slot is typed and must be defined locally in the protocol. A Protocol dictates several rules for governing the interaction and consults a Knowledge Base. The rules are SWRL implication rule instances. A knowledge base consists of a set of Propositions. Propositions are analogous to slotted facts in the conventional rule-based systems. A proposition in a knowledge base may correspond to a message that has been sent or received. Propositions are also used to represent active commitments or other domain specific facts. Figure 5 shows a possible scenario of a protocol for ordering goods (along with others, to which we refer later). For readability, a leading and trailing * is placed around external slot names, as in *amount* and *itemID*. The buyer requests a quote for an item, to which the seller responds by providing a quote. Here, a commitment is created providing semantics for the message. The commitment means that the seller guarantees receipt of the item if the buyer pays the quoted price. The buyer can either accept the quote or reject it (not shown). Again, the semantics of acceptance is given by the creation of another commitment from the buyer to pay the quoted price if it receives the requested item. Below are the rules for Order in the “antecedents ⇒ consequents” notation. contains(KB, startProp) ⇒ send(reqForQuote(?itemID)) contains(KB, reqForQuoteProp(?itemID)) ⇒ send(quote(?itemID, ?itemPrice)) ∧ createCommitment(S, CC(S, B, pay(?itemPrice), goods(?itemID))) contains(KB, quoteProp(?itemID, ?itemPrice)) ⇒ send(acceptQuote(?itemID, ?itemPrice)) ∧ createCommitment(B, CC(B, S, goods(?itemID), pay(?itemPrice))) contains(KB, quoteProp(?itemID, ?itemPrice)) ⇒ send(rejectQuote(?itemID, ?itemPrice))

DESAI et al.: INTERACTION PROTOCOLS AS DESIGN ABSTRACTIONS FOR BUSINESS PROCESSES

PAYMENT PROTOCOL Payer

Payee

ORDER PROTOCOL Gateway

paymentInfo(cardNO, expDate) CC(payer, payee, authNOKProp(error), payFine(fine))

5

Buyer

Seller reqForQuote(itemID)

authReq(cardNO, expDate, *amount*) authOK(tokenNO, amount) CC(gateway, payee, captureReqProp (tokenNO), capturedProp(amount))

quote(itemID, itemPrice) CC(s, b, pay(itemPrice), goods(itemID))

receipt(amount) captureReq(token)

acceptQuote(itemID, itemPrice) CC(b, s, goods(itemID), pay(itemPrice))

captured(amount)

SHIPPING PROTOCOL Receiver

Sender

Shipper

shipInfo(shipAddress) reqForShipOptions(shipAddress, *item*) shipperOptionQuote(shipOption, shipperQuote) CC(sh, se, payToShipperProp(shipperQuote), senderOptionQuote(shipOption, senderQuote) shipmentProp(item)) CC(se, r, payToSenderProp (senderQuote), shipmentProp(item)) chooseOption(shipOption, senderQuote) CC(r, se, shipmentProp(item), payToSenderProp(senderQuote))

shipOrder(item, shipOption, shipAddress) CC(se, sh, shipmentProp(item), payToShipperProp(shipperQuote)) shipment(item)

Fig. 5.

COMPOSITION AXIOMS 1: roleDefinition(define:Purchase.customer, unify:Order.buyer, unify:Shipping.receiver, unify:Payment.payer) 2: roleDefinition(define:Purchase.merchant, unify:Order.seller, unify:Shipping.sender, unify:Payment.payee) 3: dataFlow(definition:Order.itemID, usage:Shipping.item) 4: dataFlow(definition:Order.itemPrice, usage:Payment.amount) 5: implication(antecedent:Shipping.shipmentProp, consequent:Order.goods) 6: implication(antecedent:Payment.authOKProp, consequent:Order.pay) 7: eventOrder(earlier:Payment.authOKProp, later:Shipping.shipOrderProp)

Example: Order, Shipping, and Payment protocols and their composition

Here, reqForQuote, quote, and acceptQuote are OWL-P message instances (individuals in OWL terminology), and their corresponding proposition instances are reqForQuoteProp, quoteProp, and acceptQuoteProp. And, pay and goods are other propositions while ?itemID and ?itemPrice are native slots. Readers may notice that the ?itemID in the first rule is not assigned any value by the antecedents. It means that the rule is abstract and not executable. As we will see in Section V-B, it can be augmented with business logic that produces such values. OWL-P dictates that the rules having undefined native slots must be augmented with the business logic that produces such values. How do these rules govern the interaction? The next section describes the operational semantics of the protocol rules to answer that question. The OWL-P ontology and protocol instance examples in their RDF/XML serialization, and corresponding Prot´eg´e projects are available at http://www4.ncsu.edu/∼nvdesai/owl/. B. Operational Semantics Protocols are specified from the global perspective with an assumption of an abstract global knowledge base. Later sections show how the abstraction of a global knowledge base maps to the perspectives of the participants having their local knowledge bases. Rules are forward-chained. OWL-P defines

several property predicates with operational semantics. Table I lists the semantics for such property predicates of OWL-P. A proposition can only be retracted from a knowledge base with the use of predicates. A discharge commitment operation is automatic as stated in the Section II-A transformation 1 and hence not mentioned here. Figure 4 shows the predicates of Table I at work. For now, ignore the steps 3, 4, and 5 dealing with the policy rules. When a message is received, it is checked against the protocol rules to see if its consumption is allowed. If so, a corresponding proposition is asserted to the knowledge base and a commitment is created according to the message semantics. Update of the knowledge base may activate some other protocol rules resulting in sending of a message and assertion of corresponding proposition and commitments (if any). The examples sometimes omit the OWL-P properties, e.g., contains, send, and createCommitment when the meaning is clear. Hence, send(quote(?itemID,?itemPrice)) would be quote(?itemID,?itemPrice) and contains(KB,startProp) would be startProp. IV. C OMPOSITE P ROTOCOLS The previous section described how to specify individual protocols. However, real-world business processes would typ-

6

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

Predicate contains assert send

Domain KnowledgeBase Proposition Message

receive

Message

createCommitment

Role

Range Proposition KnowledgeBase

Commitment

Meaning Proposition ∈ KnowledgeBase ? KnowledgeBase ← KnowledgeBase ∪ Proposition Asynchronous send to the receiver assert(KnowledgeBase, MessageProp) Asynchronous receive from the sender assert(KnowledgeBase, MessageProp) assert(KnowledgeBase, CommitmentProp)

TABLE I O PERATIONAL SEMANTICS OF PROTOCOL RULES

ically involve multiple protocols. This section shows how a composite of such multiple protocols can be constructed. Conceptually, each component protocol achieves a business goal. Thus, several such protocols composed together would achieve the goals of the larger business process. Another motivation for composition is to be able to refine or amend protocols with additional rules. Because a set of additional rules is a protocol itself, the problem boils down to the problem of combining the original protocol with the amendments. Also, the ability to compose protocols would allow significant reuse of published protocols. How can we construct such composite protocols? How do they facilitate reusability? How do they allow refinements of protocols? This section answers these questions. A. Construction of Composite Protocols composedOf

2..*

1

Protocol 2..*

11

body 1

definedBy

1

1

stipulates *

Implication 1

CompositeProtocol

CompositionProfile combines

1 head

Proposition usage

CompositionAxiom

define

1

RoleDefinition unify 1..*

1

1 1 1

DataFlow

Role later

EventOrder 1

1 definition

1

1

ExternalSlot

Slot

1 earlier

1

Fig. 6.

Message 1

OWL-P composition classes and properties

Figure 6 describes the OWL-P entities and properties that deal with the problem of protocol composition. A Composite Protocol is an aggregation of component protocols and is defined by a Composition Profile. A composition profile describes the combination of two or more protocols by stipulating several Composition Axioms. Composition axioms define relationships among the protocols being combined. The operational semantics of an axiom specifies the way in which the

relationships affect the composite protocol. Figure 5 depicts an Order protocol, a Shipping protocol, a Payment protocol, and a set of composition axiom instances stating the relationships among them. In the figure and the following discussion, we denote the composition axioms as axiom1 (property1 :range1 , property2 :range2 ,. . .) where, axiom1 is an instance of a composition axiom, propertyi are the properties of the respective axiom class, and the rangei are the values of those properties. An equivalent first-order logic formulation would be property1 (axiom1 ,range1 ) ∧ property2 (axiom1 ,range2 ) ∧ . . .. We also abstract out the slot names when they are irrelevant and let a ’·’ denote their existence. A Role Definition axiom states which of the roles in the component protocols are played by the same agent, and defines the name of the unified (coalesced) role in the composite protocol. In the example, the first axiom states that the roles of a buyer in Order, a payer in Payment, and a receiver in Shipping are played by an agent who will play the role of a customer in Purchase protocol. Similarly, the second axiom defines the merchant role in the Purchase protocol. The non-unified roles must be played by different agents in the composite protocol. The instances of the roles being unified are discarded from the composite OWL-P and a new instance is added for the newly defined role. When the cardinality of the unify property is one, the axiom acts as a role renaming mechanism. A Data Flow axiom states a data-flow dependency among the protocols. A component protocol might be using a slot defined by another component protocol, possibly with a different name. Since a slot can be defined only once, and native slots must be defined inside the protocol, they cannot use a value defined by another protocol. Hence, the range of the usage property must be an external slot. In the example, the fourth axiom states that the slot ?amount in Payment gets its value from the slot ?itemPrice in Order. Such a dependency exerts an ordering among the rule defining the slot and all the rules using it, i.e., none of the the rules using the slot can fire before the slot is assigned a value by the defining rule. Thus, the operational semantics of the axiom is given as: axiom:dataFlow(definition:Order.itemPrice, usage:Payment.amount) def :reqForQuoteProp(·) ⇒ quote(·,?itemPrice) ∧ · · ·

DESAI et al.: INTERACTION PROTOCOLS AS DESIGN ABSTRACTIONS FOR BUSINESS PROCESSES

use0 :paymentInfoProp(·,·) ⇒ authReq(·,·,?amount) usei :· · · usen :captureReqProp(·) ⇒ captured(?amount) use0 :paymentInfoProp(·,·) ∧ quoteProp(·,?itemPrice) Rightarrow authReq(·,·,?amount) usei :· · · usen :captureReqProp(·) ∧ quoteProp(·,?itemPrice) ⇒ captured(?itemPrice)

The ordering is achieved by adding the definition of the slot as a premise for the usage of the slot. Since there might be multiple uses of a slot, premises of them all need to be updated. Also, the usage slot takes the name of the defining slot and the definition of external slot is discarded from composite OWL-P. An Implication axiom states that an assertion of proposition X in a component protocol implies an assertion of proposition Y in another component protocol. For example, the sixth axiom states that an assertion of authOKProp in Payment means an assertion of pay in Order. This can be easily achieved by adding an implication rule to the composite rule base. Hence, the operational semantics of the axiom is: axiom:implication(body:Payment.authOKProp, head:Order.pay) rule :authOKProp(·,·) ⇒ pay(·)

Unlike the DataFlow axiom, an EventOrder axiom explicitly specifies an ordering among the messages of the component protocols. For example, the seventh axiom states that an authOK message from the payment gateway must be received before a shipOrder message is sent to the shipper. This can be achieved by making the rule for the later event depend on the rule for the earlier event. Hence, the operational semantics of the axiom is: axiom

:eventOrder(earlier:Payment.authOK, later:Shipping.shipOrder) earlier:authReqProp(·,·,·) ⇒ authOK(·,·) ∧ CC(·,·,·,·) later :chooseOptionProp(·,·) ⇒ shipOrder(·,·,·) ∧ CC(·,·,·,·) later

:chooseOptionProp(·,·) ∧ authOKProp(·,·) ⇒ shipOrder(·,·,·) ∧ CC(·,·,·,·)

Composition axioms must be specified by a designer. There might be several ways of composing the component protocols yielding different composite protocols. As a special case, if the component protocols are completely independent of each other, no axioms need be specified and their OWL-P specifications can be simply aggregated yielding the OWL-P specification of the composite protocol. If deemed necessary, more subclasses of CompositionAxiom can be defined along with their properties and operational semantics. A composite protocol exposes its compositionProfile and possesses all the properties of the component protocols. Hence, a composite protocol itself can be a component protocol in some other

7

composition profile instance. How can we determine whether additional component protocols are needed? To answer this question, we define closed and open protocols. Definition 2: A protocol is closed if it has no external slots, and all the commitments created in the protocol can be discharged by the protocol messages. Definition 3: A protocol is open if it is not closed. A designer’s goal is to obtain a closed protocol by repeated applications of composition. Observe that in Figure 5, Order is open as its rules do not assert propositions pay and goods necessary for discharging the commitments created. Payment is open as its rules do not assert the proposition pay(fineAmount) and amount is an external slot. Shipping is open as its rules do not assert payToSenderProp and payToShipperProp, and item is an external slot. The composite Purchase is also open as its rules do not assert the propositions pay(fineAmount), payToSenderProp, and payToShipperProp. A designer would choose protocols that assert these missing propositions and combine them with Purchase to obtain a closed composite protocol. B. Refinement by Composition Business protocols evolve continually as new requirements and new features routinely arise. Therefore, the ability to systematically refine the protocols is valuable. In the composite Purchase, consider a situation in which the customer has already paid the merchant for the goods and hence the commitment C(m, c, goods(itemID) is active. However, if a fire destroys the merchant’s warehouse, the merchant will not be able to honor its commitment to ship the item. How can such exceptions be handled? The protocol could detect the violation due to an unfulfilled commitment, and the merchant could be held legally responsible. A more flexible solution would be to allow the merchant to refund the payment and release it from the commitment, provided the customer agrees to it. We can achieve this flexibility by combining Purchase with Adjustment shown in the Figure 7 and specified by the following rules: C(deb,cred,cond) ⇒ exception(?reason) exceptionProp(?reason) ⇒ OK() ∧ cancel(cred, C(deb,cred,cond)) ∧ create(cred, C(deb,cred,newCond))

The following composition axioms yield a more flexible protocol New : 1: roleDefinition(define:New.customer, unify:Purchase.customer, unify:Adjustment.creditor) 2: roleDefinition(define:New.merchant, unify:Purchase.merchant, unify:Adjustment.debtor) 3: Implication(body:Purchase.C(m,c,goods(itemID)), head:Cancel.C(deb,cred,cond)) 4: Implication(body:Cancel.C(deb,cred,newCond), head:Purchase.C(deb,cred,refund))

Adjustment

allows

cancellation

of

the

merchant’s

8

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

ADJUSTMENT PROTOCOL Debtor

Creditor

C(d, c, cond) exception(reason) OK cancel(cred, C(deb, cred, cond)) create(cred, C(deb, cred, newCond))

Fig. 7.

Handling exceptions by composition

commitment if the customer deems it reasonable. The semantics of OK message specifies cancellation of the old commitment and creation of a new commitment for compensation. The rule for sending exception message should be augmented with the merchant’s business logic such that this rule is enabled only when the exception arises. Similarly, the rule for sending OK should be augmented with the customer’s business logic such that it enables the rule only when it deems the reason valid. Note that New is open as it cannot bring about the proposition refund by itself. Similar protocols for assigning, delegating, and releasing commitments can be defined. Adding new functionalities would involve composition of a set of rules for the new requirements with the original protocol. V. P ROCESSES As described in Section II, a process is an aggregation of the local processes of participating agents. However, an OWLP specification of a protocol is a model of the interaction from a global perspective. To construct the local process of a participant, we need to derive the participant’s view of the protocol, called its role skeleton. Section V-A describes the generation of role skeletons from an OWL-P specification. A. Role Skeletons A role skeleton is one role’s view of the protocol. Here, we present an algorithm for generating role skeletons from an OWL-P protocol specification. OWL-P describes a protocol from the global perspective where the propositions are added to the global state and there are no distributed sites. The role skeletons describe the protocol from the perspective of the corresponding role. As in all distributed systems, the state of a protocol as seen by a role is changed only when a message is sent or received by that role. This observation forms the basis of our role skeletongeneration algorithm presented in Algorithm 1. The algorithm invokes the procedure getPertinentRules(P, ρ) in line 1, which gathers all rules from the OWL-P specification for protocol P that have, the role ρ receiving or sending a message. The propositions asserted by this set of rules are the only propositions that ρ will see. We denote this set of rules by ρ.rules and the set of propositions by Prop. This procedure is defined from line 6 to line 14. Next, the algorithm invokes the procedure

Algorithm 1: deriveSkeleton(P, ρ): Generate the skeleton for a role algocf 1 getPertinentRules(P, ρ) ; 2 foreach rule r in ρ.rules do 3 foreach proposition p in r.body do 4 if p is of the form CONTAINS(P.kb, atom) then 5 Replace atom with replace(atom, ρ, P ); 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24

Procedure getPertinentRules(P , ρ): Get all rules in which ρ sends or receives m ρ.rules ← {} ; foreach rule r in P.rules do foreach proposition p in r.head do if p is of the form SEND(ρ0 , ρ, m) then Replace p with RECEIVE(ρ0 , ρ, m); ρ.Rules ← ρ.rules ∪r; if p is of the form SEND(ρ, ρ0 , m) then ρ.Rules ← ρ.rules ∪r; Procedure replace(P , ρ, atom): If atom isn’t asserted in ρ.rules replace it by something that is repl ← {}; if atom is asserted by a rule rl in ρ.rules then repl ← repl ∪ atom ; return repl; if atom is asserted by a rule rg in P.rules then foreach proposition p in rg .body do if p is of the form CONTAINS(P.kb, a) then repl ← repl ∪ replace(a, ρ, P ); return repl

replace(P, ρ, atom), defined from line 15 to line 24. If a proposition atom ∈ Prop triggers a rule r ∈ ρ.rules but atom is not asserted by any rules in ρ.rules, it means that atom was not seen by ρ. This procedure replaces atom with the last proposition that ρ did see, i.e., the proposition atom0 that was asserted in ρ.rules and leads to the atom being asserted in the OWL-P specification. As an example, we show a rule in Shipping in Figure 5, and the same rule in the generated skeleton of the receiver. As the receiver would not be aware of the previous exchanges between the sender and the shipper, the antecedent of the rule for receiving senderOptionQuote should be adjusted as shown below. Protocol rule: shipperOptionQuoteProp(?shipOption,?shipperQuote) ⇒ senderOptionQuote(?shipOption,?senderQuote) ∧ CC(Se,Re,payToSenderProp(?senderQuote),shipmentProp(?item)) Receiver skeleton rule: shipInfoProp(?shipAddress) ⇒ receive(senderOptionQuote(?shipOption,?senderQuote)) ∧ CC(Se,Re,payToSenderProp(?senderQuote),shipmentProp(?item))

DESAI et al.: INTERACTION PROTOCOLS AS DESIGN ABSTRACTIONS FOR BUSINESS PROCESSES

9

C. Usage B. Policies Generation of a role skeleton is not enough to obtain a local process of a participant. As mentioned earlier, some of the rules of the protocols may be abstract, meaning that values of some of the native slots in the rule must be produced by the role’s business logic. Hence, a role skeleton must be augmented with the business logic to obtain a local process. How can we determine whether an augmented role skeleton is a local process? To answer this question, we first define concrete and abstract role skeletons, and a local process. A role skeleton is concrete if all of its native slots are defined. A role skeleton is abstract if it is not concrete. Definition 4: A local process is a role skeleton that is concrete and derived from a closed protocol. Seller skeleton rules: contains(KB, startProp) ⇒ receive(reqForQuote(?itemID)) contains(KB,reqForQuoteProp(?itemID)) ∧ quotePolicy(?itemPrice) ⇒ send(quote(?itemID, ?itemPrice)) ∧ createCommitment(S, CC(S, B, pay(?itemPrice), goods(?itemID))) contains(KB, quoteProp(?itemID, ?itemPrice)) ⇒ receive(acceptQuote(?itemID, ?itemPrice)) ∧ createCommitment(B, CC(B, S, goods(?itemID), pay(?itemPrice))) contains(KB, quoteProp(?itemID, ?itemPrice)) ⇒ receive(rejectQuote(?itemID, ?itemPrice))

Here, we show how our model of business processes can be grounded and practiced in the well established technology of service-oriented computing. Figure 8 summarizes our methodology with a scenario involving a customer interested in purchasing goods online. Software designers design protocols and register them with protocol repositories. They may also construct composite protocols by specifying composition axioms and reusing the existing component protocols from the repository. Composer is the tool developed by us for generating the composite protocol given the component protocols and the composition axioms. A merchant wishing to supply goods online looks up the repository for a suitable Purchase. It generates the skeleton for the merchant role, augments it with its local policies, and deploys the result as a service. The service profile for this service would contain an OWL-P description of Purchase. The service can be registered with a UDDI registry. If a customer wishes to procure goods online, it searches the UDDI registry, finds the merchant, and acquires the OWL-P skeleton for the customer role from the merchant. The customer enacts its local process by augmenting the skeletons with its local policies and starts interacting with the merchant. We have developed tools to support these development scenarios and a prototype implementation based on the agent architecture of Figure 4. Software Designer

specify

Merchant Skeleton OWL-P

Composer

Axioms

2

Order OWL-P

Seller’s policy for deciding quote: contains(KB, reqForQuoteProp(?itemID)) ⇒ call(policyDecider, quotePolicy(?itemID))

We propose that the business logic be specified in terms of the local policy rules of the agents. The skeleton of the seller role in Order augmented with the policy rules of the seller agent is shown above. The last rule is the policy rule which calls a business logic operation to decide how much to quote. The operation would assert the quotePolicy proposition and that would activate the second skeleton rule. Observe that this pattern of augmenting policy rules is general and will be applied to the rules where the agent has to make a decision and respond. It would also assign a value to native slots that are not defined. Figure 4 shows the interplay between the protocol rules and the policy rules of an agent. Steps 3, 4, and 5 show the policy rules in action. The business logic could involve processing such as looking up a legacy database or waiting for human input. When a message is received by the messaging interface, it is checked against the protocol rules to see whether it can be accepted, according to the protocol, at this state. For example, the seller will not receive the acceptQuote message unless it knows that a quote has been sent as shown in the third rule above.

MERCHANT

3

Shipping OWL-P

Payment OWL-P

1

register

Protocol Repository C U S T O M E R

Fig. 8.

Local Policy

+

Local Policy 6

Merchant Local Process

4 5

7

lookup

register

10

Customer Skeleton OWL-P

Purchase.Customer Skeleton

11 Customer Local Process

Purchase OWL-P

+

Merchant Port

Search Merchant

9 UDDI Repository 8

A usage scenario

VI. π-C ALCULUS F ORMALIZATION So far, we have presented our approach from a practical standpoint. We showed how our interaction-based treatment is conducive to design abstractions such as reusability and evolvability. It would help to reason about the properties of the protocols. To do so, we first introduce the π-calculus, show how protocols and their composition can be specified in it, and then describe some properties of the protocols that can be established using the π-calculus formalization. A. The π-calculus The π-calculus [18], [23] is a process algebra for modeling concurrent processes whose configurations, that is, communi-

10

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

Prefixes

α ::=

Agents

P ::=

Definitions

A(x1 , . . . , xn )

a(x) a(x) τ 0 α.P P +P P |P [x = y]P [x 6= y]P (new x)P !P Ahy1 , . . . , yn i def = P,

(Output) (Input) (Silent) (Nil) (Prefix) (Sum) (Parallel) (Match) (Mismatch) (Restriction) (Replication) (Identifier) (where i 6= j ⇒ xi 6= xj )

TABLE II π- CALCULUS S YNTAX

cation links may change as the processes execute. In the πcalculus, the fundamental unit of computation is the transfer of a communication link between two processes. Intuitively, the communication link is like an access to a resource. The simplicity of the π-calculus arises from the fact that it includes only two kinds of entities: names and agents (processes). These are sufficient to rigorously define interactional behavior. There are many variants of the π-calculus. In this paper, we shall use the synchronous π-calculus in which interaction corresponds to a handshake between two processes and involves the output of a link by one process and simultaneous receipt of the link by another process. The following briefly presents the π-calculus. The language of the π-calculus consists of prefixes and process expressions, as summarized in Table II. Below we explain the language constructs in the same order as Table II. Prefixes are of the following kinds: • The output prefix a(x) means that x is sent along the channel a. • The input prefix a(x) means that the channel a can be used to receive input and binds this input to x. • The silent τ means that nothing observable happens. The process expressions are as follows: • 0 represents the nil-process. • α.P does the action represented by prefix α and changes to P. • P + Q represents the sum-nondeterminism, that is, do either process P or process Q. • P |Q represents that process P and process Q execute in parallel. • [x = y]P or match represents the process that changes to P if x = y. Mismatch is the opposite, i.e., it checks x 6= y. • (new x)P means that the variable x is declared as a new name local to process P and bound in P. It is not visible outside of P. • !P represents an unbounded number of copies of the def process P . Formally, !P = P |!P . • Ahy1 , . . . , yn i represents the instantiation of a defined agent. def • A(x1 , . . . , xn ) = P (where i 6= j ⇒ xi 6= xj ) represents the declaration of a process A in terms of

process P. One can think of it as a method declaration in traditional procedural programming. The input prefix and the new operator bind names. For example, in the process a(x).P, the name x is bound, but a is not. A useful extension to the basic π-calculus introduced above is the ability to exchange tuples of names instead of a single name. This extended π-calculus is called the polyadic π-calculus [18]. For example, x(a, b, c) outputs three names a, b, and c over the channel x. Similarly, x(p, q, r) receives three names over x and binds them to p, q, and r respectively. We have introduced a notation for broadcasts. A broadcast on a channel x of a name y is indicated by x b(y) and is equivalent to !x(y). For an illustrative example, consider the process P given below. P ≡ (new z)(z(w).w(y)|x(u).u(v)|x(z)) The pair x(z) and x(u) can interact. P1 indicates the process left after interaction. P1 ≡ (new z)(z(w).w(y)|z(v)|0) In P1 , another interaction is possible over the channel z giving process P2 . P2 ≡ (new z)(v(y)|0|0) Process P thus evolves to P2 over two interactions - P → P1 and P1 → P2 . We use →∗ to abbreviate a series of such interactions, thus writing P →∗ P2 . B. Protocols Here, we provide the formalization of protocols in the π-calculus. Step by step, we illustrate the formalization of Order of Figure 5. Figure 9 shows a model of Payment in the π-calculus. Pipes denote the channels, boxes the π-processes, and rounded rectangles the agents. A complete formalization of Payment, Shipping, and Purchase is presented in the Appendix. A protocol is an interaction pattern among roles. The interaction is carried out via an exchange of messages which corresponds to reactions in the π-calculus. Thus, a protocol can be specified as a π-process in which each of the messages is represented by a channel. Unique names for channels corresponding to each message type are assumed. Each role skeleton is a π-process having the relevant messages as the π-process parameters. The structure of a protocol π-process would be a parallel composition of the role skeletons of each of the roles. Thus, Order would be formalized as: def

Order (b, s, rfq, quote, accept, reject, goods, pay) = Buyer hrfq, quote, accept, rejecti | Seller hrfq, quote, accept, rejecti | Commhb, s, rfq, quote, accept, reject, goods, payi

DESAI et al.: INTERACTION PROTOCOLS AS DESIGN ABSTRACTIONS FOR BUSINESS PROCESSES

11

amt ch

should check if they match for the purpose of correlation. Following is the similar π-process for the buyer role skeleton:

Payment

def

aReq

P a y e r

P a y e e

pInfo

G a t e w a y

aOK

aNok cReq

receipt cRes

pFin e

fine ch

g

pe

pr

pInfo_ pol

Commitment Management

Payer Agent Fig. 9.

Buyer (rfq, quote, accept, reject) = (new rfq pol , accept pol ) c (g).quote(g 0 , p 0 ). RFQp .rfq \ (g 0 , p 0 ) + Rejectp .r\ (Acceptp .accept eject (g 0 , p 0 ) RFQp ≡ rfq pol.rfq pol (g) Acceptp ≡ accept pol (g 0 , p 0 ).accept pol Rejectp ≡ reject pol (g 0 , p 0 ).reject pol

It is easy to see that (Buyer | Seller ) →∗ 0, provided correct behavior of the business logic for policies. This means that the role skeletons of the buyer and the seller role are compatible for interaction. The commitment semantics of the interaction is given by the observer π-process Comm as follows: def

Comm(b, s, rfq, quote, accept, reject, goods, pay) = (new ch1 , ch2 , ch3 , ch4 ) quote(g, p).CC hs, b, pay, goods, ch1 , ch2 i.(ch1 (p) | ch2 (g)) | accept(g 0 , p 0 ).CC hb, s, goods, pay, ch3 , ch4 i.(ch3 (g 0 ) | ch4 (p 0 ))

A pi-calculus model of Payment

Here, Comm is a process that observes the message exchanges and manages commitments according to the message semantics. Each role is also represented as a name, e.g., b and s. They would represent debtors and the creditors in commitments. The protocol messages are channels rfq, quote, accept , and reject. The channels goods and pay represent external messages which will be discussed later. Both role skeletons are passed all the message channels as both of the roles are involved in all the interactions. Here is the π-process for the seller role skeleton: def

Seller (rfq, quote, accept, reject) = (new quote pol ) rfq(g).Quotep .q\ uote(g, p). (accept(g 0 , p 0 ) + reject(g 0 , p 0 )) Quotep ≡ quote pol (g).quote pol (g, p)

The seller receives g (itemID) on rfq, consults its policy for quoting and sends the quote price p (itemPrice) on quote, and receives either accept (acceptQuote) or reject (rejectQuote). Quotep is a stub for interacting with the quoting policy which would be part of the business logic of the seller agent, using the channel quote pol . Such policy stubs output necessary names to the corresponding policy channel which would be received by the business logic, and then receive some new names output by the business logic on the same channel. As the policies are private to the agents, the channels for interacting with them are restricted to the skeleton π-process, e.g., quote pol . As g is bound by rfq, a new name g 0 should be bound to the input on accept or reject. Similarly as p is bound by quote pol , p0 binds to the input on accept or reject. Usually, g and g 0 would receive the same input but it cannot be guaranteed. Ideally, the seller

On a message exchange that affects a commitment, Comm would call the corresponding commitment operation π-process. Here, the commitments are created when quote or accept is observed according to their semantics. After calling the π-process CC for a conditional commitment, necessary message parameters are passed to it. The π-process CC is given as follows: def

CC (deb, cred , cond1 , cond2 , ch1 , ch2 ) = (new ch3 , ch4 , ch5 ) (ch1 (val1 ) | ch2 (val2 )).(cond2 (val20 ).([val2 6= val20 ] CC hdeb, cred , cond1 , cond2 , ch3 , ch4 i.(ch3 (val1 ) | ch4 (val2 ))+ [val2 = val20 ]τ ) + cond1 (val10 ).([val1 = val10 ] C hdeb, cred , cond2 , ch5 i.ch5 (val2 ) + [val1 6= val10 ] CC hdeb, cred , cond1 , cond2 , ch3 , ch4 i.(ch3 (val1 ) | ch4 (val2 ))))

First, the parameters passed by Comm are received, and then the channels related to the commitment conditions are observed. On an exchange, if the commitment condition is satisfied then the process ends. If the precondition is satisfied, the conditional commitment reduces to a commitment, the π-process C is called, and necessary parameters are passed. If neither is satisfied, CC is called again and the commitment remains active. Private channels chi are used for passing parameters to avoid interference with the protocol channels. The commitment conditions may involve varying number of parameters and CC needs to be defined accordingly. The given definition is for the case when both the precondition and the condition have one parameter. Similarly, the π-process C is given as follows: def

C (deb, cred , cond2 , ch2 ) = (new ch3 )ch2 (val2 ). (cond2 (val20 ).([val2 = val20 ]τ + [val2 6= val20 ] C hdeb, cred , cond2 , ch3 i.ch3 (val2 )))

The separation of the commitment semantics from the inter-

12

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

action specification simplifies the derivation of role skeletons, e.g., the buyer role skeleton is the parallel composition of the π-processes Buyer , Comm, CC , and C . Also, the lose coupling among the commitment semantics, the interaction specification, and the policy definitions (business logic) allows maintainability, reusability, and simplicity of design.

of the event order axiom is taken, i.e., it does not enforce the condition actively but it allows us to decide if the message ordering is violated. Figure 10 shows a model of Purchase. Customer Agent

Merchant Agent

Gateway Agent

Shipper Agent

C. Composite Protocols

se

sh

re

g

pe

pr

s

b

accept

Order

Shipping

Payment

shipment

item ch

amt ch

goods

aOK

Axiom4 Axiom7

def

paySh

paySe

pF ine

Axiom3 fine ch

Axiom5

Axiom6

Purchase(c, m, g, sh, . . . order channels . . . , . . . payment channels . . . , def . . . shipping channels . . . = Order hc, m, . . .i | Paymenthc, m, g, . . .i | Shippinghc, m, sh, . . .i | Axiom4 haccept, amtch i | Axiom6 haOK , payi | Axiom7 haOK , shipmenti | . . . other axioms . . .

Purchase

pay

Here, a formalization of the protocol composition in the π-calculus is presented. A composite protocol is a parallel composition of the component protocols and the composition axioms, e.g, Purchase can be composed as follows:

\ (p) Axiom4 (msg, channel ) = msg(g, p).channel def

Fig. 10.

A pi-calculus model of Purchase

Axiom6 (msg1 , msg2 ) = msg1 (tNO, amt).msg2 (amt) def

Axiom7 (msg1 , msg2 ) = msg1 (·, ·).msg2 (·, ·, ·)

A complete formalization is given in the Appendix. The channels c, m, g, and sh are the roles of Purchase. Notice how passing these channels to Order , Payment, and Shipping accomplishes role unification; role definition axioms are not needed. The axiom numbers relate to the axioms in Figure 5. A Data Flow axiom is a π-process with two parameters. The first parameter is the channel that defines a name and the second parameter is the channel that uses the defined name. The axiom receives on the defining channel and forwards it to the using channel, e.g., Axiom4 receives the price on the accept channel and outputs the price to the amtch , i.e., the channel on which the users of amt in Payment listen for the definition. Note that the broadcast is needed as there might be multiple listeners. An Implication axiom is a π-process with two parameters. The first parameter is the antecedent of the implication and the second parameter is the consequent. The axiom listens on the antecedent channel, and on the message exchange, signals by outputting to the consequent channel, e.g., Axiom6 listens on aOK to see if the payment is authorized and, signals so to pay when it is authorized. An Event Order axiom is a π-process with two parameters. the first parameter is the channel that should exchange the message first and the second parameter is the channel that should follow, e.g., Axiom7 expresses the condition that pay should exchange before shipment does. Here, a passive view

The dotted pipes are the protocol channels and the axioms listen on them. Agent business logics and the policy channels are not shown. It is encouraging to see how the protocols can be coupled with each other through their external channels via composition axioms. Clearly, Purchase itself can be a component protocol in another composition. D. Properties of Protocols We showed how protocols can be formalized in the πcalculus. However, the significance of such a formalization depends on the kinds of inferences it allows. What inferences can we make about the protocols due to the formalization? Here, we describe such inferences, leaving the proofs for future work. In the following, Proti is a protocol π-process definition, Roleij is the role skeleton definition of role j in Proti , and chik is an external channel k for protocol Proti . Subscripts i, j, k, m, n and so on range over the cardinality of the respective entity, e.g., Rolemn could represent a role skeleton π-process for role n in a protocol Protm . Also, S is the weak simulation relation and ≈ is the weak bisimulation relation. Here, we assume desirable functioning of the business logic by replacing each Policyp by τ . 1) Incorrectness: A protocol specification Prot1 causes a commitment violation if Prot1 | ch11 | · · · | ch1k →∗ C. The debtor of C is responsible for the violation. A protocol specification Prot1 causes an interaction violation

DESAI et al.: INTERACTION PROTOCOLS AS DESIGN ABSTRACTIONS FOR BUSINESS PROCESSES

if Prot1 | ch11 | · · · | ch1k →∗ C | Role1j . A protocol specification Prot1 causes an event ordering violation if Prot1 | ch11 | · · · | ch1k →∗ Axiomi , and Axiomi is an event order axiom. A protocol specification Prot1 is incorrect if it causes either of the above violations. Note that correctness of a specification can only be verified relative to requirements. The definition of incorrectness given here is general and applies regardless of the requirements. 2) Compatibility: Role skeletons Roleij and Rolemn are compatible if Roleij | Rolemn | ch11 | · · · | chpq →∗ 0. Although this definition is intuitive, in case of iterative interactions, the process would never reduce to a nil process as suggested by Canal et al. [7]. In that case, Role skeletons Roleij and Rolemn are compatible if Roleij | Rolemn | ch11 | · · · | chpq continues making τ transitions without interacting with its environment. 3) Equivalence: Protocols Prot1 and Prot2 are equivalent if Prot1 ≈ Prot2 . Due to the presence of policy stubs in the protocol specification, the equivalence is defined by the weak bisimulation with policy interactions as τ transitions. 4) Flexibility: A protocol Prot1 is more flexible than a protocol Prot2 if (Prot2 , Prot1 ) ∈ S and (Prot1 , Prot2 ) ∈ / S. Note that this also implies Prot2 can be replaced by Prot1 . Other property of interest might be commitment equivalence of the protocols to see if two protocols are equivalent as far as the commitment semantics of the interaction goes. Also, a relation between a protocol and its refined version can be defined to see if one of them is a specialization of the other, e.g, payment by credit card is a specialized version of a payment protocol. We believe that the formalization is rich enough to allow such inferences. VII. R ELATED W ORK Several areas of research are relevant to our work. We discuss each of them briefly and highlight the key differences. Component behavior modeling: Plasil et al. [20] propose a language based on regular expressions for describing the behavior of software components using protocols. They define software components as agents and the proposed language allows expressions of method invocations over components. Their behavior protocols are similar to our business protocols but do not entertain commitment-based semantics of the interactions. Similarly, Canal et al. [7] use π-calculus to describe protocols over the methods provided of CORBA objects. They reason about interaction compatibility and object substitutability, that is, if one object can be successfully substituted by another. Whereas, their goal is to be able to verify designs for correctness and substitutability of components, our main thrust is an interaction-based business process development methodology that allows reuse, refinement, and aggregation. Scenario-Based behavior modeling: A lot of the work in this area has focused on developing visual formalisms with semantics and applying them for modeling interaction

13

scenarios of entities. Popular interaction modeling formalisms include AUML [2], Message Sequence Charts [13], and UML sequence diagrams [14]. Entities may be agents, components, or processes. The work by Whittle et al. [29] presents an approach for coming up with a design model from a collection of interaction scenarios using a state-identification approach for merging scenarios. Their design models are specified in the statecharts [11]. Similarly, Uchitel et al. [27] present a versatile approach for scenario-based specification, synthesis, and analysis. Their important contribution is an MSC language to explicitly specify the assumptions under which the scenarios are merged. Our protocol composition approach can be seen as an alternative to the state-identification and scenario composition techniques for merging behavior models. An important difference is that while these approaches merge a collection of behaviors to entail an interaction protocol, protocol composition merges a collection of such interaction protocols entailing a composite protocol. Also, since our methodology is aimed for business protocols, we have employed commitment semantics which these approaches do not consider in their models. Service composition: BPEL [4] is a language for specifying the static composition of Web services. However, it mixes the interaction activities with the business logic making it unsuitable for reuse. OWL-S [9], which includes a process model for Web services uses semantic annotations to facilitate dynamic composition. A composed service is produced at runtime based on constraints. While dynamic service composition has some advantages, it assumes a perfect markup of the services being composed. Dynamic composition in OWL-S involves ontological matching between inputs and outputs. Such a matching might be difficult to obtain automatically given the heterogeneity of the web. For this reason, we do not emphasize dynamic service composition. Our goal is to provide a human designer with tools to facilitate service composition. Unlike BPEL, which specifies the internal orchestration of services, WSCI [30] specifies the conversational behavior of a service using control flow constructs. However, these specifications lack a semantics, which makes them difficult to compose and reuse. Several other approaches aim to solve the service composition problem by emphasizing formal specifications to achieve verifiability. Solanki et al.[26] employ interval temporal logic to specify and verify ongoing behavior of a composed service. Their use of “assumption” and “commitment” (different meaning than here) assertions allows better compositionality than other approaches. Gerede et al.[8] treat services as activity-based finite automata to study the decidability of composability and existence of a lookahead delegator given a set of existing services. However, these approaches consider neither the autonomy of the partners, nor the flexibility of composition. Agent-Oriented software engineering: Agent-Oriented software methodologies aim to apply software engineering principles in the agent context. These include Gaia, KAOS, MaSE, and SADDE [3]. Tropos [5] includes an early requirements stage in the process. Gaia [32] describes roles in the software system being developed and identifies processes that

14

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

they are involved in as well as safety and liveness conditions for the processes. It incorporates protocols under the interaction model and can be used with commitment protocols. Ba¨ına et al. [1] advocate a model-driven Web service development approach to ensure compliance between a service’s implementation and its external protocol specifications. Our work differs from these in that it is aimed at achieving protocol reusability by separation of protocols and policies and it addresses the problem of protocol compositions. Component catalogs: Our methodology advocates and enables reuse of protocols as building blocks of business processes. Protocols can not only be composed, they can also be systematically refined to yield more robust protocols. Such protocols can be published for reuse by other designers, which is in accordance to the spirit of Commercial off-theshelf (COTS) software. Mallya and Singh [16] treat these concepts formally. The MIT Process Handbook [17], in a similar vein, catalogs different kinds of business processes in a hierarchy. For example, sell is a generic business process. It can be qualified by sell what, sell to who, and so on. Our notion of a protocol hierarchy bears similarity with the Handbook. RosettaNet [22] is similar to our approach in that it centers around publishing protocols and designing the business processes around them. However, it is currently limited to two-party request-response interactions called Partner Interface Processes (PIPs). Importantly, the PIPs lack a formal semantics.

VIII. C ONCLUSIONS This paper presented an approach for designing processes that recognizes the fundamental interactive nature of open environments where the autonomy of the participants must be preserved. Published protocols can be readily reused and combined with different policies. Commitments provide the basis for a semantics of the actions of the participants, thereby enabling the detection of violations and making the resultant protocols flexible. The significance of this work derives from the importance of processes in modern business practice. Over 100 limited business protocols have been defined in RosettaNet [22]. The presented approach will enable the development and usage of an ever-increasing set of protocols for critical business functions. We demonstrated the practicality of our approach by grounding it in a framework for specifying protocols. We also demonstrated how our approach is theoretically founded in the π-calculus. Not only is this approach conducive to reuse, refinement, and aggregation but it has also been implemented in terms of prototype tools. In future, the properties of the protocols could be proven by leveraging the pi-calculus formalization. An experiment to build an industry-scale software from protocols and policies would be interesting to study the scalability and costeffectiveness of our approach. The enterprises using the published protocols would have their organizational contexts. Enabling protocols to inherit such contexts and behave accordingly would also be an interesting research challenge.

ACKNOWLEDGMENT This research was sponsored by NSF grant DST-0139037 and a DARPA project. R EFERENCES [1] K. Ba¨ına, B. Benatallah, F. Casati, and F. Toumani. Model-driven web service development. In Proceedings of Advanced Information Systems Engineering: 16th International Conference, CAiSE, June 2004. [2] B. Bauer, J. Muller, and J. Odell. Agent UML: A Formalism for Specifying Multiagent Interaction. Springer-Verlag, 2001. [3] F. Bergenti, M.-P. Gleizes, and F. Zambonelli, editors. Methodologies and Software Engineering for Agent Systems. Kluwer, 2004. [4] BPEL. Business process execution language for web services, version 1.1, May 2003. www106.ibm.com/developerworks/webservices/library/ws-bpel. [5] P. Bresciani, A. Perini, P. Giorgini, F. Guinchiglia, and J. Mylopolous. Tropos: An agent-oriented software development methodology. Journal of Autonomous Agents and Multi-Agent Systems, 8(3):203–236, May 2004. [6] A. W. Brown. Large-Scale, Component Based Development. PrenticeHall, 2000. [7] C. Canal, L. Fuentes, E. Pimentel, J. M. Troya, and A. Vallecillo. Adding roles to corba objects. IEEE Transactions on Software Engineering, 29(3):242–259, March 2003. [8] C¸aˇgdas¸ Evren Gerede, R. Hull, O. Ibarra, and J. Su. Automated composition of e-services: Lookaheads. In Proceedings of the International Conference on Service Oriented Computing, 2004. [9] DAML-S. DAML-S: Web service description for the semantic Web. In Proceedings of the 1st International Semantic Web Conference (ISWC), July 2002. Authored by the DAML Services Coalition, which consists of (alphabetically) Anupriya Ankolekar, Mark Burstein, Jerry R. Hobbs, Ora Lassila, David L. Martin, Drew McDermott, Sheila A. McIlraith, Srini Narayanan, Massimo Paolucci, Terry R. Payne and Katia Sycara. [10] E. J. Friedman-Hill. Jess, the Java expert system shell, 1997. herzberg.ca.sandia.gov/jess. [11] D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987. [12] I. Horrocks, P. F. Patel-Schneider, H. Boley, S. Tabet, B. Grosof, and M. Dean. SWRL: A semantic web rule language combining OWL and RuleML, May, 2004 (W3C Submission). http://www.w3.org/Submission/2004/SUBM-SWRL-20040521/. [13] ITU. Message Sequence Charts, Recommendation z.120. International Telecommunication Union, Telecomminication Standardization Sector, 1996. [14] I. Jacobson, J. Rumbaugh, and G. Booch. The Unified Software Development Process. Addison Wesley, 1999. [15] JADE. Java agent development framework, 1997. http://jade.tilab.com/. [16] A. U. Mallya and M. P. Singh. A semantic approach for designing commitment protocols. In Proceedings of the AAMAS-04 Workshop on Agent Communication, July 2004. To appear. [17] T. W. Malone, K. Crowston, and G. A. Herman, editors. Organizing Business Knowledge: The MIT Process Handbook. MIT Press, Cambridge, MA, 2003. [18] R. Milner. Communicating and Mobile Systems: the pi-Calculus. Cambridge University Press, 1999. [19] OWL. Web ontology language, Feb 2004. http://www.w3.org/TR/2004/REC-owl-features-20040210/. [20] F. Plasil and S. Visnovsky. Behavior protocols for software components. IEEE Transactions on Software Engineering, 28(11):1056–1076, 2002. [21] Prot´eg´e. The prot´eg´e ontology editor and knowledge acquisition system, 2004. http://protege.stanford.edu/. [22] RosettaNet. Home page, 1998. www.rosettanet.org. [23] D. Sangiorgi and D. Walker. The pi-calculus: A Theory of Mobile Processes. Cambridge University Press, 2001. [24] SET. Secure electronic transactions (SET) specifications, 2003. http://www.setco.org/ set specifications.html. [25] M. P. Singh. An ontology for commitments in multiagent systems: Toward a unification of normative concepts. Artificial Intelligence and Law, 7:97–113, 1999. [26] M. Solanki, A. Cau, and H. Zedan. Augmenting semantic web service descriptions with compositional specification. In Proceedings of the International World Wide Web Conference, pages 544–552, 2004. [27] S. Uchitel, J. Kramer, and J. Magee. Synthesis of behavioral models from scenarios. IEEE Transactions on Software Engineering, 29(2):99– 115, February 2003.

DESAI et al.: INTERACTION PROTOCOLS AS DESIGN ABSTRACTIONS FOR BUSINESS PROCESSES

[28] M. Venkatraman and M. P. Singh. Verifying compliance with commitment protocols: Enabling open Web-based multiagent systems. Autonomous Agents and Multi-Agent Systems, 2(3):217–236, Sept. 1999. [29] J. Whittle and J. Schumann. Generating statechart designs from scenarios. In In the Proceedings of International Conference on Software Engineering, pages 314–323, 2000. [30] WSCI. Web service choreography interface 1.0, July 2002. wwws.sun.com/ software/ xml/ developers/ wsci/ wsci-spec-10.pdf. [31] WSDL. Web Services Description Language, 2002. http://www.w3.org/TR/wsdl. [32] F. Zambonelli, N. R. Jennings, and M. Wooldridge. Developing multiagent systems: The gaia methodology. ACM Transactions on Software Engineering Methodology, 12(3):317–370, 2003.

15

B. Shipping Shipping(re, se, sh, shInfo, rfso, shoq, seoq, choose, shOrder , def shipment, itemch , paySh, paySe) = Receiver hshInfo, seoq, choose, shipment, itemch i | Sender hshInfo, rfso, shoq, seoq, choose, shOrder , shipment, itemch i | Shipper hrfso, shoq, shOrder , shipmenti | Commhre, se, sh, shInfo, rfso, shoq, seoq, choose, shOrder , shipment, itemch , paySh, paySei def

A PPENDIX Here, the π-calculus formalizations of Payment and Shipping of Figure 5 are presented followed by the formalization of the composite Purchase.

A. Payment

Receiver (shInfo, seoq, choose, shipment, itemch ) = (new shInfo pol , choosep ol )itemch (item). \ ShInfop .shInfo(shAdd ).seoq(shOp, seq). \ Choosep .choose(shOp, seq).shipment(item 0 )

Sender (shInfo, rfso, shoq, seoq, choose, shOrder , def shipment, itemch ) = (new rfso pol , seoq pol , shOrder pol ) shInfo(shAdd ).itemch (item).Rfsop .[ rfso(shAdd , item). shoq(shOp, shq).Seoqp .seoq d (shOp, seq).choose(shOp, seq). \ (item, shOp, shAdd ) shOrderp .shOrder

Payment(pr , pe, g, pInfo, aReq, aOK , aNOK , receipt, cReq, cRes, def Shipper (rfso, shoq, shOrder , shipment) = def amtch , pFine, finech ) = Payer hpInfo, receipt, amtch i | (new shoq pol , shipment pol )rfso(shAdd , item). PayeehpInfo, aReq, aOK , aNOK , receipt, cReq, cRes, amtch i [ (shOp, shq).shOrder (item 0 , shOp, shAdd 0 ). Shoqp .shoq | GatewayhaReq, aOK , cReq, cResi | \ (item 0 ) Shipmentp .shipment Commhpr , pe, g, pInfo, aReq, aOK , aNOK , receipt, cReq, cRes, amtch , pFine, finech i Comm(re, se, sh, shInfo, rfso, shoq, seoq, choose, shOrder , def def shipment, itemch , paySh, paySe) = Payer (pInfo, receipt, amtch ) = (new pInfo pol ) (new ch1 , ch2 , ch3 , ch4 , ch5 , ch6 , ch7 , ch8 ) \ amtch (amt).PInfop .pInfo(cNO, exp).receipt(amt 0 ) (shoq(shOp, shq).CC hsh, se, paySh, shipment, ch1 , ch2 i. def itemch (item).(ch1 (shq) | ch2 (item))) | Payee(pInfo, aReq, aOK , aNOK , receipt, cReq, cRes, amtch ) = (seoq(shOp, seq).CC hse, re, paySe, shipment, ch3 , ch4 i. (new aReq pol , receipt pol , cReq pol ) itemch (item).(ch3 (seq) | ch4 (item))) | [ (cNO 0 , exp 0 , amt). pInfo(cNO 0 , exp 0 ).amtch (amt).AReqp .aReq (choose(shOp, seq).CC hre, se, shipment, paySei. 0 0 \ (amt ) | (aOK (tNO, amt ).(Receiptp .receipt item (item).(ch 5 (item) | ch6 (seq))) | ch 00 [ (tNO).cRes(amt )) + aNOK (tNO, error )) CReqp .cReq (shOrder (item, shOp, shAdd ). def CC hse, sh, shipment, paySh, ch7 , ch8 i. Gateway(aReq, aOK , cReq, cRes) = ch7 (item) | ch8 (shq))) (new aOK pol , aNOK pol , cRes pol )aReq(cNO, exp, amt). 0 0 00 [ (tNO, amt ).cReq(tNO ).CResp .cRes(amt [ (AOKp .aOK )+ ShInfop ≡ shInfo pol (item).shInfo pol (shAdd ) \ (error )) ANOKp .aNOK Rfsop ≡ rfso pol .rfso pol Shoqp ≡ shoq pol(shAdd , item).shoq pol (shOp, shq) Comm(pr , pe, g, pInfo, aReq, aOK , aNOK , receipt, cReq, cRes, Seoqp ≡ seoq pol (shOp, shq).seoq pol (shOp, seq) def amtch , pFine, finech ) = (new ch1 , ch2 , ch3 , ch4 ) Choosep ≡ choose pol(shOp, seq).choose pol (pInfo(cNO, exp).CC hpr , pe, aNOK , pFine, ch1 , ch2 i. ShOrderp ≡ shOrder pol .shOrder pol (amtch (amt) | finch (fine)).(ch1 (cNO, exp, amt) | ch2 (fine))) Shipmentp ≡ shipment pol.shipment pol | (aOK (tNO, amt 0 ).CC hg, pe, cReq, cRes, ch3 , ch4 i. 0 (ch3 (tNO) | ch4 (amt ))) PInfop ≡ pInfo pol (amt).pInfo pol (cNO, exp) AReqp ≡ aReq pol .aReq pol AOKp ≡ aOK pol (cNO, exp, amt).aOK pol (tNO, amt 0 ) ANOKp ≡ aNOK pol (cNO, exp, amt).aNOK pol (error ) Receiptp ≡ receipt pol .receipt pol CReqp ≡ cReq pol .cReq pol CResp ≡ cRes pol (tNO 0 , amt 0 ).cRes pol (amt 00 )

C. Purchase Purchase(c, m, g, sh, rfq, quote, accept, reject, goods, pay, pInfo, aReq, aOK , aNOK , receipt, cReq, cRes, payFine, amtch , finech , shInfo, rfso, shoq, seoq, choose, def shOrder , shipment, itemch , paySh, paySe) = Order hc, m, rfq, quote, accept, reject, goods, payi |

16

DRAFT: TSE SPECIAL ISSUE ON INTERACTION AND STATE-BASED MODELING

Paymenthc, m, g, pInfo, aReq, aOK , aNOK , receipt, cReq, cRes, payFine, amtch , finech i | Shippinghc, m, sh, shInfo, rfso, shoq, seoq, choose, shOrder , shipment, itemch , paySh, paySei | Axiom3 haccept, itemch i | Axiom4 haccept, amtch i | Axiom5 hshipment, goodsi | Axiom6 haOK , payi | Axiom7 haOK , shipmenti def \ (g) Axiom3 (msg, channel ) = msg(g, p).channel def \ (p) Axiom4 (msg, channel ) = msg(g, p).channel def

Axiom5 (msg1 , msg2 ) = msg1 (item).msg2 (item) def

Axiom6 (msg1 , msg2 ) = msg1 (tNO, amt).msg2 (amt) def

Axiom7 (msg1 , msg2 ) = msg1 (tNO, amt).msg2 (item, shOp, shAdd )