In order to analyze the behavior, the Promela model should be closed. A closed model consists of the Promela process to simulate the environment in which the target BPEL process is supposed to execute. Actually the environment contains all the service providers with which the BPEL process has communication via the appropriate partner links. As discussed in Section 3. It requires a static analysis to introduce appropriate predicate variables VP.
As briefly discussed with a simple example, the analysis is basically a define-use chain du-chain of variables having effects on the control flow. Further, a single predicate variable is introduced for each conditional expression.
Although the example in Figure 2 is simple, the translation of the receive activity might be interesting. It requires two predicate variables logically related. The fragment relevant to the discussion here follows. The variable predl denotes to the expression request.
The d-location of predl is at the receive activity where it is assigned a new value to the variable request. Although it is simple, it can be seen that a du-chain analysis calculates a correct causal relationship between the two locations. The next thing is to determine the value. However, the best to say is that the variable predl would be either true or false because the variable request is not determined at the analysis time.
Above is inserted the code fragment to set the variable predl non-deterministically either one. Once the value of predl is assigned, the search algorithm used in the model-checking method of SPIN can explore all the possible combination of the values.
In order to handle DPE properly, the set that the link variable takes as its value extends to have forced. The forced value is generated and flowed downward exactly when the DPE starts. If the activity has a join condition, the forced value is interpreted as false in the evaluation of the condition. If the activity does not have a join condition, the coming forced value makes the activity not executed but is further flowed down along the outgoing link s of the activity. Some details can be found elsewhere [ll].
The serializable scope specifies multiple concurrent accesses to the variables inside the scope are serialized. The serializable scope should be considered to form a critical region. The Promela version introduces a mutex for each such serializable scope for mutually exclusive accesses to the variables in the critical region. According to the standard coding style, the Promela code fragment to make accesses to the shared variables looks as below.
Table l presents a summary of the experiment. The four cases are taken from the BPEL standard document [2].
The last column shows the number of states in the analysis using the SPIN model-checker. Although its exact value is not significant, the number shows roughly how the analysis is complicated. As discussed in Section 5. The third example Loan Approval contains five activities executing concurrently, the state-space becomes large due to the interleaving semantics of the concurrency.
Each example employs particular language features in BPEL. Since their values are not determined, abstraction is essential. This example also needs the abstraction of variables having effects on the evaluation of the transition conditions. In each case, an appropriate environment Promela description is introduced. The environment process is constructed manually so that it adds little effects on the size of the state-space.
As discussed in Section 4. For the third example Loan Approval Figure 2 , a property that either assign or invoke 2 , not both, is executed can be checked by expressing as below.
This paper is the report of the first successful results that can analyze all the four examples in the document [2]. The key point is that the proposed method takes into account of such interesting features as DPE and the abstraction of control variables.
Thanks to using the EFA as the intermediate representation, the proposed method is clearly understood in two points: 1 to define what the behavioral specification of BPEL programs is, and 2 to clearly state the verification problem at hand.
Further, X. Fu et al [6] employs the guarded automaton model, which is essentially the same as the EFA in this paper. Both can use variables and the transition may have guard condition.
Such extended automata is a good to for the behavioral analysis of BPEL application programs. In addition, most of them do not care much about the abstraction on the control variables, and do not introduce techniques such as the predicate abstraction. The analysis results may have more false negatives than the approach in this paper. Such a false negative sometimes appears as a result of the overapproximation ignoring the causal relationships between the variables having effects on the execution control.
Unfortunately not all the BPEL programs can be analyzed with the proposed method. It does not deal with the semantics of handlers such as exception or compensation. Since handlers are the important language constructs having much effects on the behavioral specifiation of BPEL programs, incorporating such features in the analysis method is essential.
It is one of the futre work. Last, the tool discussed in the paper uses the SPIN as its back-end engine, and will be combined with the method in [12] for the analysis of the potential information leakage in BPEL application programs. Curbera et al. Version 1. Foster, S. Uchitel, J. Magee, and J. Model-based Verification of Web Service Compositions. In Proc. ASE , September Graf and H. CAV'97, pages 72 - 83, Fu, T. Bultan, and J. WWW , pages , May Verification of Business Processes for Web Services.
On Verifying Web Service Flows. In Trans. The binding of a correlation set is triggered by a specially marked message send or receive operation. A correlation set can be initiated only once during the lifetime of the scope it belongs to. Thus, a global correlation set can only be initiated at most once during the lifetime of the process instance.
Its value, once initiated, can be thought of as an alias for the identity of the business process instance. A local correlation set is available for binding each time the corresponding scope starts, but once initiated must retain its value until the scope completes. In multiparty business protocols, each participant process in a correlated message exchange acts either as the initiator or as a follower of the exchange.
The initiator process sends the first message as part of an operation invocation that starts the conversation, and therefore defines the values of the properties in the correlation set that tag the conversation. All other participants are followers that bind their correlation sets in the conversation by receiving an incoming message that provides the values of the properties in the correlation set. Both initiator and followers must mark the first activity in their respective groups as the activity that binds the correlation set.
The examples in this section show correlation being used on almost every messaging activity receive, reply, and invoke. A given message can carry multiple correlation sets. After a correlation set is initiated, the values of the properties for a correlation set must be identical for all the messages in all the operations that carry the correlation set and occur within the corresponding scope until its completion.
This correlation consistency constraint MUST be observed in all cases of initiate values. The legal values of the initiate attribute are: "yes" , "rendezvous" , "no". The default value of the initiate attribute is "no". If the constraint is violated, the semantics is undefined. If multiple correlation sets are used in a message activity, then the consistency constraint MUST be observed for all correlation sets used. For example, the correlation sets used in an inbound message activity e. If one of initiated correlation set does NOT match with the message, the semantics is undefined.
Following is an extended example of correlation. Note that these properties are global names with known simple XMLSchema types. They are abstract in the sense that their occurrence in messages needs to be separately specified see Message Properties.
The example continues by defining purchase order and invoice messages and by using the concept of aliasing to map the abstract properties to fields within the message data identified by selection. Both the properties and their mapping to purchase order and invoice messages will be used in the following correlation examples. Correlation set names are used in invoke, receive, and reply activities see Invoking Web Service Operations and Providing Web Service Operations , in the onMessage branches of pick activities, and in the onEvent variant of event handlers see Pick and Message Events.
These sets are used to indicate which correlation sets i. The initiate attribute is used to indicate whether the set is being initiated. When the attribute is set to "yes" the set is initiated with the values of the properties occurring in the message being sent or received. Please see the beginning of this section for details of of initiate attribute. These ideas are explained in more detail in the context of the use of correlation in the rest of this example.
A message can carry the tokens of one or more correlation sets. The first example shows an interaction in which a purchase order is received in a one-way inbound request and a confirmation including an invoice is sent in the asynchronous response. The PurchaseOrder correlationSet is used in both activities so that the asynchronous response can be correlated to the request at the buyer. The receive activity initiates the PurchaseOrder correlationSet. The buyer is therefore the initiator and the receiving business process is a follower for this correlationSet.
The invoke activity sending the asynchronous response also initiates a new correlationSet Invoice. The business process is the initiator of this correlated exchange and the buyer is a follower.
The response message is thus a part of two separate conversations, and forms the bridge between them. Alternatively, the response might have been a rejection such as an "out-of-stock" message , which in this case terminates the conversation correlated by the correlationSet PurchaseOrder without starting a new one correlated with Invoice. Note that the initiate attribute is missing.
It therefore has the default value of "no". The use of correlation with synchronous Web Service invocation is illustrated by the alternative synchronous purchasing operation used by an invoke activity used in the buyer's business process. Note that an invoke consists of two messages: an outgoing request message and an incoming reply message. The correlation sets applicable to each message must be separately considered because they can be different.
In this case the PurchaseOrder correlation applies to the outgoing request that initiates it, while the Invoice correlation applies to the incoming reply and is initiated by the reply. Because the PurchaseOrder correlation is initiated by an outgoing message, the buyer is the initiator of that correlation but a follower of the Invoice correlation because the values of the correlation properties for Invoice are initiated by the seller in the reply received by the buyer.
Each activity has optional standard attributes: a name and an indicator whether a join fault should be suppressed if it occurs. See Flow for a full discussion of these two attributes. When the suppressJoinFailure attribute is not specified for an activity, it inherits its value from its closest enclosing activity or from the process if no enclosing activity specifies this attribute.
The use of these elements is required for establishing synchronization relationships through links see Flow. Each link is defined independently and given a name. If the transition condition is omitted, it is deemed to be present with the constant value true. If no join condition is specified, the join condition is the logical OR of the link status of all incoming links of this activity see Invoking an operation on such a service is a basic activity.
An asynchronous invocation requires only the input variable of the operation because it does not expect a response as part of the operation see Providing Web Service Operations. A synchronous invocation requires both an input variable and an output variable. However, these attributes are both syntactically optional since they are absolutely required only in executable processes.
In the case of a synchronous invocation, the operation might return a WSDL fault message. Such a fault can be caught locally by the activity, and in this case the specified activity will be performed. If a fault is not caught locally by the activity it is thrown to the scope that encloses the activity see Scopes and Fault Handlers.
In WSDL 1. This limits the ability to use fault-handling mechanisms to deal with invocation faults. Finally, an activity can be associated with another activity that acts as its compensation action. This compensation handler can be invoked either explicitly or by the default compensation handler of the enclosing scope see Scopes and Compensation Handlers.
The name of such an implicit scope is always the same as the name of the activity it encloses. See Correlation for an explanation of the correlation semantics. The following example shows an invocation with a nested compensation handler. Other examples are shown throughout the specification. A business process provides services to its partners through receive activities and corresponding reply activities. A receive activity specifies the partner link it expects to receive from, and the port type optional and operation that it expects the partner to invoke.
In addition, it may specify a variable that is to be used to receive the message data received. However, this attribute is syntactically optional since it is absolutely required only in executable processes.
In addition, receive activities play a role in the lifecycle of a business process. The default value of this attribute is "no". A receive activity annotated in this way MUST be an initial activity in the process, that is, the only other basic activities may potentially be performed prior to or simultaneously with such a receive activity MUST be similarly annotated receive activities.
It is permissible to have the createInstance attribute set to "yes" for a set of concurrent initial activities. In this case the intent is to express the possibility that any one of a set of required inbound messages can create the process instance because the order in which these messages arrive cannot be predicted. Compliant implementations MUST ensure that only one of the inbound messages carrying the same correlation set tokens actually instantiates the business process usually the first one to arrive, but this is implementation dependent.
The other incoming messages in the concurrent initial set MUST be delivered to the corresponding receive activities in the already created instance. Note that receive is a blocking activity in the sense that it will not complete until a matching message is received by the process instance.
The semantics of a process in which two or more receive actions for the same partnerLink, portType, operation and correlation set s may be simultaneously enabled is undefined.
For the purposes of this constraint, an onMessage clause in a pick and an onEvent event handler are equivalent to a receive see Pick and Message Events. It is worth pointing out that race conditions may occur in business process execution. Messages that target a particular process instance may arrive before the corresponding receive activity is started.
For example, it is perfectly reasonable to model a process that receives a series of messages in a while loop where all the messages use the same correlation. At run time, the messages will arrive independent of the iterations of the loop.
But the fact that the correlation is already initiated should enable the runtime engine and messaging platform to recognize that these messages are correlated to the process instance and handle those messages appropriately.
For another example, a process may invoke a remote service, initiate a correlation set for an expected callback message, and the callback message may arrive before the corresponding receive activity is started for a variety of reasons. The correlation data in the arriving message should enable the engine to recognize the message is targeted for this process instance and handle it appropriately. Process engines may employ different mechanisms to handle such race conditions. This specification does not mandate any specific mechanism.
For the purposes of handling race conditions, an onMessage clause in a pick and an onMessage event handler are equivalent to a receive see Pick and Message Events. A reply activity is used to send a response to a request previously accepted through a receive activity.
Such responses are only meaningful for synchronous interactions. An asynchronous response is always sent by invoking the corresponding one-way operation on the partner link. A reply activity may specify a variable that contains the message data to be sent in reply.
The correlation between a request and the corresponding reply is based on the constraint that more than one outstanding synchronous request from a specific partner link for a particular portType, operation and correlation set s MUST NOT be outstanding simultaneously. The semantics of a process in which this constraint is violated is undefined.
For the purposes of this constraint, an onMessage clause in a pick is equivalent to a receive see Pick. If the response to the request is normal, the faultName attribute is not used and the variable attribute, when present, will indicate a variable of the normal response message type.
If, on the other hand, the response indicates a fault, the faultName attribute is used and the variable attribute, when present, will indicate a variable of the message type for the corresponding fault. A reply activity is associated with a inbound message activity based on the tuple - partnerLink, operation, and messageExchange. The value defined in messageExchange is scoped to the combination of partnerLink and operation. That is, it is legal to use the same messageExchange value in multiple simultaneously incomplete receive activities so long as the combination of partnerLink and operation on the receives are all different from each other.
If there should ever be multiple simultaneous incomplete inbound message activities which have the same partnerLink, operation and messageExchange tuple then the bpws:conflictingRequest fault MUST be thrown within the BPEL process on the conflicting inbound message activities subsequent to the execution of the successful incomplete receive. If a reply activity cannot be associated with an incomplete receive activity by matching the tuples and this error situation is not caught during static analysis, then bpws:missingRequest fault MUST be thrown within the BPEL process on the reply activity.
If the messageExchange attribute is not specified on a receive then its value is taken to be empty. For matching purposes two empty messageExchange values with the same partnerLink and operation values are said to match. Empty value does not match with other non-empty values. Variable update occurs through the assignment activity, which is described in Assignment.
The throw activity can be used when a business process needs to signal an internal fault explicitly. Every fault is required to have a globally unique QName. The throw activity is required to provide such a name for the fault and can optionally provide a variable of data that provides further information about the fault. A fault handler can use such data to analyze and handle the fault and also to populate any fault messages that need to be sent to other services.
An application or process-specific fault name can be directly used by using an appropriate QName as the value of the faultName attribute and providing a variable with the fault data if required. This provides a very lightweight mechanism to introduce application-specific faults.
A simple example of a throw activity that does not provide a variable of fault data is:. The wait activity allows a business process to specify a delay for a certain period of time or until a certain deadline is reached see Expressions for the grammar of duration expressions and deadline expressions.
A typical use of this activity is to invoke an operation at a certain time in this case a constant, but more typically an expression dependent on process state :. There is often a need to use an activity that does nothing, for example when a fault needs to be caught and suppressed. The empty activity is used for this purpose. The syntax is obvious and minimal. Structured activities prescribe the order in which a collection of activities take place.
They describe how a business process is created by composing the basic activities it performs into structures that express the control patterns, data flow, handling of faults and external events, and coordination of message exchanges between process instances involved in a business protocol.
There are cases where one activity can replace another. For example, the sequence activity, used to structure sequential processing, may be emulated by a properly configured flow with additional links. The purpose in providing what are, strictly speaking, redundant activities is to make it easier for BPEL process designers to both read and write BPEL processes using familiar, even if functionally redundant, activity constructs.
Structured activities can be used recursively in the usual way. A key point to understand is that structured activities can be nested and combined in arbitrary ways.
This provides a somewhat unusual but very attractive free blending of the graph-like and program-like control regimes that have traditionally been seen as alternatives rather than orthogonal composable features.
A simple example of such blended usage is found in the Initial Example. It is important to emphasize that the word activity is used throughout the following to include both basic and structured activities. The sequence activity completes when the final activity in the sequence has completed. The switch structured activity supports conditional behavior in a pattern that occurs quite often. The activity consists of an ordered list of one or more conditional branches defined by case elements, followed optionally by an otherwise branch.
The case branches of the switch are considered in the order in which they appear. The first branch whose condition holds true is taken and provides the activity performed for the switch.
If no branch with a condition is taken, then the otherwise branch is taken. If the otherwise branch is not explicitly specified, then an otherwise branch with an empty activity is deemed to be present. The switch activity is complete when the activity of the selected branch completes.
The while activity supports repeated performance of a specified iterative activity. The iterative activity is performed as long as the given Boolean while condition holds true at the beginning of each iteration. The pick activity awaits the occurrence of one of a set of events and then performs the activity associated with the event that occurred. The occurrence of the events is often mutually exclusive the process will either receive an acceptance message or a rejection message, but not both.
If more than one of the events occurs, then the selection of the activity to perform depends on which event occurred first. If the events occur almost simultaneously, there is a race and the choice of activity to be performed is dependent on both timing and implementation. Note that after the pick activity has accepted an event for handling, the other events are no longer accepted by that pick.
A special form of pick is used when the creation of an instance of the business process could occur as a result of receiving one of a set of possible messages. In this case, the pick itself has a createInstance attribute with a value of yes the default value of the attribute is no.
No alarms are permitted for this special case. The semantics of the onMessage event is identical to a receive activity regarding the optional nature of the variable attribute, the handling of race conditions, and the constraint regarding simultaneous enablement of conflicting receive actions. For the last case, recall that the semantics of a process in which two or more receive actions for the same partner link, portType, operation and correlation set s may be simultaneously enabled is undefined see Providing Web Service Operations.
Enablement of each onMessage handler is equivalent to enablement of the corresponding receive activity for the purposes of this constraint. For details, see Providing Web Service Operations. The pick activity completes when one of the branches is triggered by the occurrence of its associated event and the corresponding activity completes.
The following example shows a typical usage of pick. Such a pick activity can occur in a loop that is accepting line items for a large order, but a completion action is enabled as an alternative event. The flow construct provides concurrency and synchronization. The grammar for flow is:. The standard attributes and standard elements for activities nested within a flow are especially significant because the standard attributes and elements primarily exist to provide flow-related semantics to activities.
The most fundamental semantic effect of grouping a set of activities in a flow is to enable concurrency. A flow completes when all of the activities in the flow have completed.
Completion of an activity in a flow includes the possibility that it will be skipped if its enabling condition turns out to be false see Dead-Path-Elimination. Thus the simplest use of flow is equivalent to a nested concurrency construct.
In the following example, the two invoke activities are enabled to start concurrently as soon as the flow is started. The bank is invoked only after the flow completes. More generally, a flow activity creates a set of concurrent activities directly nested within it. It further enables expression of synchronization dependencies between activities that are nested directly or indirectly within it.
The link construct is used to express these synchronization dependencies. A link has a name and all the links of a flow activity MUST be defined separately within the flow activity. The standard source and target elements of an activity are used to link two activities. The source of the link MUST specify a source element specifying the link's name and the target of the link MUST specify a target element specifying the link's name.
If the transition condition is omitted, it is deemed to be present with a value of "true". This is described further in Every link declared within a flow activity MUST have exactly one activity within the flow as its source and exactly one activity within the flow as its target.
Moreover, at most one link may be used to connect two activities; that is, two different links MUST NOT share the same source and target activities. Finally, the source and target of a link MAY be nested arbitrarily deeply within the structured activities that are directly nested within the flow, except for the boundary-crossing restrictions. The following example shows that links can cross the boundaries of structured activities.
There is a link named "CtoD" that starts at activity C in sequence Y and ends at activity D, which is directly nested in the enclosing flow. The example further illustrates that sequence X must be performed prior to sequence Y because X is the source of the link named "XtoY" that is targeted at sequence Y.
A link is said to cross the boundary of a syntactic construct if the source or target activity for the link is nested within the construct while the link is declared outside the construct. Note that it is possible for a link to cross the boundary of a syntactic construct even in those cases where both the source and the target activities are nested within the same construct so long as the link is declared outside that construct.
A link MUST NOT cross the boundary of a while activity, a serializable scope, an event handler or a compensation handler see Scopes for the specification of event, fault and compensation handlers.
In addition, a link that crosses a fault-handler boundary MUST be outbound, that is, it MUST have its source activity within the fault handler and its target activity within a scope that encloses the scope associated with the fault handler. Finally, a link MUST NOT create a control cycle, that is, the source activity must not have the target activity as a logically preceding activity, where an activity A logically precedes an activity B if the initiation of B semantically requires the completion of A.
Therefore, directed graphs created by links are always acyclic. In the rest of this section, the links for which activity A is the source will be referred to as A's outgoing links, and the links for which activity A is the target will be referred to as A's incoming links.
If activity X is the target of a link that has activity Y as the source, X has a synchronization dependency on Y. This applies even when an activity has exactly one incoming link. If the explicit join condition is missing, the implicit condition requires the status of at least one incoming link to be positive see below for an explanation of link status.
A join condition is a Boolean expression see Expressions. The expression for a join condition for an activity MUST be constructed using only Boolean operators and the bpws:getLinkStatus function see Expressions applied to incoming links at the activity. Without considering links, the semantics of business processes, scopes, and structured activities determine when a given activity is ready to start.
For example, the second activity in a sequence is ready to start as soon as the first activity completes. An activity that defines the behavior of a branch in a switch is ready to start if and when that branch is chosen. Similarly, an activity nested directly within a flow is ready to start as soon as the flow itself starts, because flow is fundamentally a concurrency construct.
If an activity that is ready to start in this sense has incoming links, then it does not start until the status of all its incoming links has been determined and the implicit or explicit join condition associated with the activity has been evaluated. The link status is a tri-state flag associated with each declared link. This flag may be in the following three states: "positive", "negative", or "unset". Each time a certain flow activity is activated, the link status of all the links declared in that activity is "unset", that is the lifetime of the status of a link is exactly the lifetime of the flow activity within which it is declared.
The precise semantics of link status evaluation are as follows:. When activity A completes, the following steps are performed to determine the effect of the synchronization links on other activities:. The status will be either positive or negative. To determine the status for each link its transitionCondition is evaluated. International Conference on Internet Computing. Computer Science, Engineering. Enabling high quality executable domain specific language specification. View 1 excerpt, cites background.
Certification of transformation algorithms in model-driven software development. Software Engineering. Effective and Efficient Process Engine Evaluation. View 4 excerpts, cites background. Denotational fixed-point semantics for constructive scheduling of synchronous concurrency. Acta Informatica. Despite the popularity of BPEL engines to orchestrate complex and executable processes, there are still only few approaches available to help find the most appropriate engine for individual … Expand.
The paper presents a comprehensive and integrated approach for business process modeling and for the specification of distributed business application systems.
0コメント