CASE STUDY 1

The case study concerns a typical online auction process, which consists of three participants: the online auction system and two buyers, A₁ and A₂.A seller owes a good that wants to sell to the highest possible price. Therefore, he introduces the product in an auction system for a certain time. Then, buyers (or bidders) may place bids for the product and, when time runs out,the highest bid wins. In our case, we suppose the resource is the product for auction, the value of the resource property is the current price (only the auction system can modify it), the resource subscribers will be the buyers, their subscription conditions hold when the current product value is higher than their bid, and the resource lifetime will be the time in which the auction is active.

Finally, when the lifetime has expired, the auction system sends a notification to the buyers with the result of the process (the identifier of the winner, v_w) and, after that, all the processes finish.

The formal description and the BPEL-WSRF for the case study
can be found here:

    The CPNTools model for the case study can be found here:

    The source code in xml can be found here:

CASE STUDY 2

The case study concerns a typical automatic management system for stock market investments, which consists of four participants: the online stock market system and three investors, A₁, A₂ and A₃ . Here, the resource will be the stocks of a company that the investors want to buy just in case the price falls below an established limit, which the investors ?x previously by means of subscriptions, i.e., an investor subscribes to the resource (the stocks) with a certain guard (the value of the stocks he/she want to pay for it). The lifetime will be determined by the stock market system and the resource price will be ?uctuating to simulate the rises/drops of the stock. Notice that we do not take into account the stock buy process since our aim is to model an investors’ information system. Thus, the participants will be noti?ed when their bids hold or the resource lifetime expires.

The formal description and the BPEL-WSRF for the case study
can be found here:

    The CPNTools model for the case study can be found here:

    The source code in xml can be found here: