Recently, a promising programming model called Orc is proposed to support a structured way of orchestrating distributed web services. Orc is intuitive because it offers concise constructors to manage concurrency communication, time-outs, priorities, failure of sites or communication and etc. The semantics of Orc is also precisely defined.

• Associate Professor and Assistant Dean: Jin Song Dong
• Graduate Student: Yang Liu
• PhD Candidate: Jun Sun
• Graduate Student: Xian Zhang

Orc is as well precise and elegant. Both operational semantics and denotational semantics (a tree semantics are defined. However, as a new emerging language, there is no formal model-checking technique to systematically verify critical properties over systems modeled in Orc. Orc roots in traditional process algebra and there are works on applying model checking technique to process algebra, therefore we believe that existing mature model-checkers can be reused instead of building one from scratch. In this work, we address the verification problem of the Orc language. Our aim is to detect possible violations of critical properties, especially timing properties, of Orc programs using existing mature model checker. Our approach starts with defining an executable model in Timed Automata for Orc expressions, which conforms the operational semantics of the Orc language. As a natural consequence, existing tool supports for Timed Automata, e.g. Uppaal, can be used for verification of Orc models. The dining philosophers example is used as a running example to demonstrate our approach. Moreover, we implement a tool to construct Uppaal models automatically from Orc model, as a demonstration that our approach can be fully automated.

Orc has a strong theoretical foundation in process algebra, particularly CCS, CSP and p-calculus. These process algebra provide fundamental models of concurrency in which processes communicate over channels. However, Orc is different from above process algebra as Orc permits integration of arbitrary components (sites) in a computation. This introduces a distinction between the Orc expression and the environment in which it runs. More importantly, Orc has timing control to handle the site failures. Traditional process algebra have well established model checking theories and tool support, e.g. FDR2 for CSP, CWB-NC for CCS, etc. Because of the absence of quantitative timing support, none of these tools can model and verify timing aspects of complex systems. There are some process algebra with time extensions, for example, Timed CCS and Timed CSP. Unfortunately, there is no good model checker available.

Timed Automaton is a notation developed for modeling and verification of real-time systems. It is a specialized finite state machine with clocks. Well developed automatic verification tools are available for Timed Automata, like Uppaal, KRONOS, TEMPO and RED. This gives the inspiration of this work. Our Timed Automata semantics for Orc would allow Timed Automata verification techniques, theories and tools, to be applied to Orc, instead of building them all from scratch.

Business process orchestration languages, like XML based BPEL4WS, share many common elements with Orc. Both BPEL4WS and Orc treat a controlling process and the services they orchestrate differently. Both languages provide mechanisms for parallel execution and sequencing. Several recent works address the verification problem of BPEL4WS. Model-based verification of BPEL4WS models web services work flows using the Finite State Processes notation, which is then verified using their tool LTSA-WS. Pu and his colleagues defined an operational semantics for BPEL4WS as well as a transformation from BPEL4WS to Timed Automata. Uppaal is then used to verify the Timed Automata. As Orc is more abstract and has well-defined semantics, our work therefore focuses on defining an equivalent semantics for Orc in Timed Automata so as to use existing tools.

Implementation

We developed an experimental tool to automatically construct Uppaal models from Orc models using XML and Java technology. There is not yet a standard interchange format for Orc. Therefore, we start with defining the syntax of Orc using XML schema, which is available here. The XML schema are carefully defined to express any Orc models in a structured text document as well as to force some wellformedness using XML constraints. Together with the XML schema, a parser and a transformation module is built using Java and SAX parser to parse XML representations of Orc and construct respective Uppaal model automatically. The output of the program is an XML representation of the Uppaal model, which is readily to be employed and verified in Uppaal. The Uppaal model construction flowchart is shown in Figure 1.

Figure 1. First Implementation

After our first implementation, Orc Programming System is created by Jayadev Misra and William R. Cook. By using their Orc language parser, we can directly construct the Uppaal model without the XML schema translation step. The new Uppaal model construction flowchart is shown in Figure 2.

Figure 2. New Implementation

We briefly mention some of the Uppaal model construction implementation issues here. Because Uppaal does not allow data pass through channels, global variables are carefully defined to pass along the values, i.e. a publish event is always attached with an assignment to the respective global variable. An aggressive simplification procedure is applied whenever possible to simplify and somehow optimize the constructed Timed Automata. For instance, when we apply Definition 4.3 Sequential Composition, if we are certain there is only one copy of g required, we may do the product of the two automata and remove the publish event given that it does not affect the rest of the model. We as well try to minimize the number of clock variable via reusing the same one as so to speed up the verification. However, the simplification and optimization remains as a challenge task and we may improve it by considering Orc laws.

Orc language can be evaluated using Orc Programming System. In our implementation, we integrate this function in our tool Orc2Uppaal, where the Orc program can be loaded or input in the interface Figure 3, hence evaluated. The main function of our tool is the Uppaal model construction. After input the Orc program, the corresponding Uppaal program will be generated after clicking the construction button. The Uppaal program can be saved into disk, then verified using Uppaal. One future work is to integrate the Uppaal verification library to our system, so the Orc program can be easily verified within one interface.

Program

• Download: Orc2Uppaal.exe
  • To run it, simply unpack into any directory and run the Orc2Uppaal.exe
    
  • You need J2SE 1.5 in order to run Orc2Uppaal.exe, because Orc2Uppaal uses the generic feature.
    

Source Code

• The high-level design of the Orc implementation is given in Implementation Outline of Orc.
• Code documentation: javadoc
• Source files: Orc2Uppaal.zip
  • This tool is implemented using Jbuilder 2005. This zip file contains an Jbuilder package for building Orc2Uppaal.
  • Orc2Uppaal.exe is built using Native Executable Builder in JBuilder.
  • All libraries used are stored under folder lib. They need to be included if the source code is compiled in other IDEs.

• Dining Philosopher

• Online Auction System

Dining Philosopher

There are N Philosophers, sitting around a table. Every pair of neighbors shares a fork. The fork to the left of Philosopher i is Fork_i and to his right is Fork_i' . Philosopher i can eat only if it holds both left and right forks. A philosopher's life cycle consists of following activities: acquire the two adjacent forks, eat, and release the forks. Because of the seating arrangement, neighboring philosophers can not eat simultaneously.

Each Fork_i modelled as a FIFO buffered channel which is either empty (if some philosopher holds the corresponding fork) or has one signal (if no philosopher holds the fork). We write Fork_i.put to send a signal along the channel. Initially, each channel holds a signal. In this example, P_i (0 <= i < N) depicts philosopher i, where the right neighbor of P_i is P_i' (i' = (i + 1) mod N), and Eat returns a signal on completion of eating.

The behaviors of the forks in the dining philosopher are modelled as Figure 3, where the user may repeatedly get the fork and then put it back. Consequently, a site call Fork_i.put is interpreted as a synchronization on the call_{Fork_i.out} (simplified as Fork_i.put in this example). For an abstract site call like Eat, instead of building a trivial automaton which synchronizes on the call event and then returns a signal, it is treated as an abstract local event for the sake of efficient verification.

Figure 3. Timed Automaton for Fork_i

Figure 4. Network of Automata for P_i (1 <= i <= N)

Finally Figure 5 shows the Timed Automata for P_i. the automata network for DP in the dining philosopher is the network containing the networks in Figure 4 (one for each i).

Figure 5. Timed Automata for P_i

Online Auction System

Purchase Order Handling System

Purchase Order Handling System handles purchase order from a customer. On receiving the purchase order, the process initiates three tasks concurrently: calculating the final price for the order, selecting a shipper, and scheduling the production and shipment for the order. While some of the processing can proceed concurrently, there are control and data dependencies between the three tasks. In particular, the shipping price is required to finalize the price calculation, and the shipping date is required for the complete fulfillment schedule. When the three tasks are completed, invoice processing can proceed and the invoice is sent to the customer. The workflow of the purchase order handling is shown in Figure 6.

Figure 6. Purchase Order Workflow

The list of the web services in this example are explain as follows:

ProduceInv(price, prodSchd)

Generate the invoice using the calculated price and production schedule.

InitPriceCal()

Initialize the price calculation.

GetPrice(shpInfo)

Complete the price calculation based on the shipping information. The final price is returned.

InitProdSchd()

Initialize the production scheduling.

GetProdSchd(shpSchd)

Complete the production scheduling based on shipping schedule. The production schedule is returned.

GetShpInfo(custInfo)

Return the shipping information based on the customer information.

GetShpSchd(shpInfo)

Return the shipping schedule based on the shipping information.

MailInv(inv, custInfo)

Mail the invoice inv to the customer.

The Orc program of purchase order is defined as follows. The first definition GetInv describes the workflow in Figure 6. The second definition describes the Purchase Order handling system: Mail the invoice to the customer if the GetInv returns the invoice with the t time units, otherwise return an error massage to customer.

The definition of GetInv is a little much more complex than the picture, because the the data dependency of the shipping information and shipping schedule. The nested where clauses are used to enforce the order of the shipping site calls as well as the current execution of the InitPriceCal, InitProdSchd and GetShpInfo.

The Uppaal model of the purchase order handling system is shown as following picutures. We can see clear the two shipping site calls are merged into one process, because the syncronization call publish_shpInfo and publish_prodSchd blocks the

Figure 7. Get Price Process

Figure 8. Get Shipping Data Process

Figure 9. Get Production Schedule Process

Figure 10. Get Invoice Process

Figure 11. Timeout Process

Figure 12. Purchase Order System Process

Last updated 02/20/2006.