A Precise Description of the S-BPM Modeling Method

This chapter presents a precise formulation of the S-BPM constructs discussed in the preceding chapters. We express them in the form of an abstract SBD-interpreter, which yields a precise, controllable definition of the subject behavior in SBDs, the so-called semantics of SBDs. Furthermore, this definition establishes a solid scientific foundation for the S-BPM method to support a guarantee of the implementation correctness of the interpreter by the Metasonic modeling tool.

This chapter presents a precise formulation of the S-BPM constructs discussed in the preceding chapters. We express them in the form of an abstract SBDinterpreter, 1 which yields a precise, controllable definition of the subject behavior in SBDs, the so-called semantics of SBDs. Furthermore, this definition establishes a solid scientific foundation for the S-BPM method to support a guarantee of the implementation correctness of the interpreter by the Metasonic modeling tool. 2 The correctness of the interpreter model concerns two levels: correctness of the interpreter with respect to the intended meaning of the modeling constructs (ground model correctness) and correctness of the interpreter implementation by the tool with respect to the interpreter (refinement correctness). Thus, the interpreter model represents a blueprint of the system and the double-faced correctness guarantees that the user understanding of processes and the result of their machine executions match, a feature that is crucial for reliable computer supported modeling systems.
Due to the survey character of this chapter, we only review here the main S-BPM modeling constructs and refer for a complete version of the interpreter model to the appendix.

Abstract State Machines
A precise definition of the meaning of business process modeling constructs provides a reliable basis for successful communication between the different stakeholders, namely designers and analysts on the management, development, and evaluation level, IT-specialists and programmers on the implementation level, and users on the application level. This needs a language that is common to the involved parties and allows to avoid the well-known problems of ambiguity of natural languages. This holds in particular for the S-BPM approach whose fundamental concepts-actors, which perform arbitrary actions on arbitrary objects and communicate with other actors-require most general heterogeneous data structures: sets of various elements with various operations and predicates (properties and relations) defined for them and agents, which execute those operations.
for M(x/a), where a denotes the value of t in the given state and M(x/a) is obtained from M by substitution of each (free) occurrence of x in M by a.
For details of a mathematical definition of the semantics of ASMs which justifies their intuitive (rule-based or pseudo-code) understanding, we refer the reader to the AsmBook (Börger and Stärk 2003). It contains also an explanation of the so-called refinement method which we use here to define the components of the SBDinterpreter in steps-a didactical concern adopted already in the preceding chapters of this book.

Interaction View of SBD-Behavior
An S-BPM process (short process) is defined as set of agents each of which is equipped with an SBD so that the process behavior can be defined by the SBDbehavior of its subjects (see Sect. 5.5.5). Thus, the definition of an S-BPM process interpreter as asynchronous ASM is reduced to the definition of a sequential ASM, which represents the interpreter BEHAVIOR subj (D) of an arbitrary subject subj in an arbitrary SBD-diagram D. For the interpretation of a process, this interpreter can then be replicated (read: instantiated) with each corresponding SBD.
A subject walks from node to node along the edges of D, beginning at the start node, and executes at each node the associated service until it reaches an end state. Therefore, the total behavior of the subject in D can be defined as set of each local BEHAVIOR(subj, node) of the subject at this node of D: BEHAVIOR subj (D) ¼ {BEHAVIOR(subj, node) | node 2 Node(D)} In this way, one can define SBD-computations of subj in the usual way as sequences S 0 ,. . ., S n of (data) states of subj in the diagram which begin with an initial state S 0 , i.e., a data state which has an initial SID-state, 5 lead to a state S n with a final SID-state and where each state S i+1 is obtained from S i with SID-state state i by a step of BEHAVIOR(subj, state i ).
Thus, the construction of an interpreter is decomposed into the definition of the behavior of a subject in a given state, represented in the diagram by a node, for each type of state. This directly supports the intuitive operational understanding of the single S-BPM constructs and simplifies the interpreter definition. Before proceeding to this definition in Sect. 12.3.2, we list in Sect. 12.3.1 the assumptions we make for the diagrams.

Diagrams
An SBD is a directed graph. Each node represents a state where a subject which is in this state performs the associated action service(node). We call such a state an SID-state (Subject Interaction Diagram state) and denote it by SID_state (subj) since the abstract interpretation of service (node) refers only to the role the state plays with respect to other subjects with which subject communicates from within D. We speak without distinction about states as nodes.
Each SID-state has one of three types corresponding to the type of the associated service: function state (also called internal function or action state), send state, or receive state. Each SID-state is implicitly parameterized with the SBD in which it occurs, sometimes denoted by an index as in SID_state D (subject) and SID_state (subject, D). Each SID-state is part of the encompassing so-called data state or simply state (read: the underlying Tarski structure of the SBD).
The edges which enter or exit a node represent the SID-state transitions from the source node source(edge) to node resp. from node to the target node target(edge). Therefore, we call the target(outEdge) of an outEdge (an element of OutEdge (node)) also a successor state of node (in the diagram an element of the set Successor (node)) and source (inEdge) of an inEdge 2 InEdge (node) a predecessor state (an element of the set Predecessor(node)). A transition from a source to a target node is permitted only if the execution of the service associated to the source node is Completed so that each outgoing edge corresponds to a termination condition of the service and is typically indicated on the edge as ExitCond. We write ExitCond i for the ExitCond of the i-th outgoing edge if there is more than one.
Each SBD is finite and has exactly one initial and one end state. Each path is required to lead to at least one end state. It is permitted that an end state may have outgoing edges; a process terminates only if each of its subjects is in an end state.

SID-View of State Behavior
For the definition (of the SID-view) of BEHAVIOR (subject, state), see Fig. 12.1. It describes the transition subject has to perform from a SID_state with associated service A to a next SID_state with associated service B i once the execution of A (using an abstract machine PERFORM) is Completed, where subject upon entering a state must START the associated service. The successor state target(outEdge (state, i)) with its associated service B i is determined via a function select Edge ; it can be defined by the designer or at runtime by the executing subject. The following ASM-rule provides a compact textual description where the elsecase expresses that it may take many steps until the execution of PERFORM for A by the executing subject is terminated.
is a scheme which comes with abstract machines PERFORM, START, and an abstract termination criterion Completed as components. It describes the interaction view of an SBD-that a subject upon entering a node STARTS the associated action and PERFORMS its steps until Completed becomes truewithout providing details on how the component machines work and how they satisfy the termination criterion. The three constituents can and must be specified further to make the meaning of the performed action concrete. We do this in the next two sections for the S-BPM communication actions. The extension for the additional behavioral S-BPM constructs is given in the appendix.

Choice of Alternative Communication Steps
In this section, we define what it means to bring one step out of a set of so-called alternative communication steps to its execution. In this description, the meaning of a single such step still remains abstract and is refined in Sect. 12.5 by details of their multiprocess communication capabilities. In Sect. 12.4.1, we define the elements of the characteristic S-BPM input pool concept and formulate in Sect. 12.4.2 the first refinement of START, PERFORM, and Completed for sending and receiving; here the multiprocess communication capability still remains abstract. Since many definitions are symmetric in sending and receiving, we formulate them using a parameter ComAct for the corresponding Communication Action.

Basics of the Input Pool Concept
To support asynchronous communication, which is typical for distributed systems, each subject has an inputPool(subj) where other subjects in the sender role may deposit messages and where subject in the receiver rule "expects" messages (i.e., looks for messages when it is ready to receive some).
Each inputPool can be configured by capacity bounds for the maximal number of messages it may contain of a specific or an arbitrary type and/or from a specific or arbitrary sender. All four possible cases (read: parameter pairs of arbitrary or specific type and sender) are considered (see Sect. 5.5.5.2).
To obtain a uniform description also for synchronous communication, 0 is allowed as value for the capacity parameters of an input pool. It is interpreted as requiring that the receiver expects to receive messages of the indicated type and/or from the indicated sender only via a rendezvous with the sender.
Asynchronous communication is determined by positive natural numbers for the input pool capacity parameters. Two strategies are contemplated for the case that a sender tries to deposit a message in an input pool that has reached already its corresponding capacity: • Canceling send where either (a) a message is deleted from the input pool to enable the insertion of the incoming message or (b) the incoming message is thrown away (not inserted into the input pool). • Blocking send where sending the message is blocked and the sender must repeat the attempt to send this message until either (a) an appropriate place has become free in the input pool, or (b) a timeout interrupts the attempt to send the message, or (c) the sender decides to abrupt the attempt to send the message.
For the first case, two versions to cancel are contemplated, namely to delete from the input pool the message which is Present there for the longest resp. shortest time, as described by two functions oldestMsg and youngestMsg defined in the appendix.
Whether an attempt to send is treated by an input pool P of the receiver as canceling or blocking is a question of whether in the given state the capacity condition of P would be violated by inserting the incoming message. These conditions are given by a constraintTable(P) in which the i-th row indicates for a combination of sender i and msgType i the allowed maximal number size i of messages of this kind, together with the action i to be performed in case of a capacity violation: constraintTable (inputPool) ¼ . . . sender i msgType i size i action i (1 i n) . . . where action i 2 {Blocking, DropYoungest, DropOldest, DropIncoming} size i 2 {0,1, 2, . . .,1 } sender i 2 Subject msgType i 2 MsgType When a sender attempts to deposit a msg in P the first row ¼ s t n a in constraintTable(P) is identified (if there is one) whose capacity bound is relevant for msg and would be violated by inserting msg:

ConstraintViolation(msg, row) iff 6
Match (msg, row) ∧ size ({m 2 P | Match (m, row)}) + 1 > n where Match(m, row) iff (sender(m) ¼ s or s ¼ any) and (type(m) ¼ t or t ¼ any) If there is no such row, the message can be inserted into P. Otherwise the action indicated in the identified row is performed so that either this attempt to send is blocked or the message is accepted via a cancellation action (possibly by directly throwing away the message).
It is required that each row with size i ¼ 0 satisfies action i ¼ Blocking and that if maxSize(P) < 1 holds, then the constraintTable contains the following default-row: any any maxSize Blocking Similarly, a receiver tries to transfer from its input pool into its data space an "expected" message (i.e., a message of the indicated (msgType, sender)) as we will see when interpreting a receive step.
In a distributed process at a given moment, multiple subjects may try to deposit a message in the input pool P of a same receiver, but only one subject can obtain the access to the resource P. Therefore, a selection mechanism is needed to determine this subject. We use a function select P which allows one to define the access predicate as follows: CanAccess(sender, P) iff sender ¼ select P ({subject | TryingToAccess(subject, P)})

Iteration Structure of Alternative Communication Steps
In an alternative communication state, a subject performs the requested communication action ComAct by executing, until the communication succeeds (see Sects. 5.5.4.3 and 5.5.4.4), the following three steps, where Alternative(subj, node) is the set of all ComAct-alternatives the subject finds in the given state node: • Selection: Choose from Alternative (subj, node) an alternative communication kind. • Preparation: Prepare a msgToBeHandled which corresponds to the chosen alternative, that is in case of ComAct ¼ Send a concrete msgToBeSent and otherwise a concrete expectedMsg kind. • ComAct-attempt: TRYALTERNATIVE ComAct , i.e., try-synchronously or involving the input pool-to send the concrete msgToBeSent resp. to accept a message that Matches the expectedMsg kind.
The first two steps (choice and preparation of the alternative) are done by a component CHOOSE&PREPAREALTERNATIVE ComAct which represents the first step of TRYALTERNATIVE ComAct and is defined in Sect. 12.5.1.
If the third step fails for the chosen alternative, that is if msgToBeHandled cannot be sent resp. received neither asynchronously nor synchronously, the subject repeats the three steps for the next alternative until: • Either ComAct succeeds for some alternative and the subject can set the predicate Completed for the ComAct (i.e., the service) in the given state node to true. • Or TryRoundFinished holds, that is all alternatives have been tried without success.
In the second case, after this first so-called nonblocking round, further rounds of ComAct-attempts are started which are blocking in the sense that they can be terminated, besides by being normally Completed, also by a Timeout or by a UserAbruption. Timeout has higher priority than UserAbruption.
The set RoundAlternative of still to be tried alternatives must be initialized for each round to Alternative (subj, node). This happens: • For the nonblocking-round in START.
• For the first blocking-round in INITIALIZEBLOCKINGTRYROUNDS, where also the Timeout-clock is set. • For each further round in InitializeRoundAlternatives.
Since the blocking rounds can be interrupted, to continue the computation via PROCEED the SBD must contain at least three edges leaving node to be taken after a normal or a forced ComAct-termination. Three predicates NormalExitCond, TimeoutExitCond, and AbruptionExitCond determine the outgoing edge which must be taken to reach the next SID-state if COMACT is normally Completed or ends by a Timeout or a UserAbruption. These three predicates are initialized in START, namely to false.
The following definition of PERFORM (subj, ComAct, state) synthesizes the preceding explanations in symbolic form. We write it down in the form of a traditional flowchart in Fig. 12.2. Such diagrams represent ASMs and thus have a precise semantics [see Börger et al. (2003, p. 44) and the equivalent textual definition in the appendix, where also the other more or less obvious and therefore here not listed component machines are defined].
Macros and Components of PERFORM(subj,ComAct, state). We define here START(subj, ComAct, state), INTERRUPT, and ABRUPT and refer for the other components to the appendix. START

MultiProcess-Communication
In this section, we refine TRYALTERNATIVE ComAct (and thereby by one more level of detail also PERFORM (subj, ComAct, state)) by a definition of the elements which enable this component for multiprocess communication in S-BPM (see Sect. 5.6.4).
As said in Sect. 12.4.2, the first TRYALTERNATIVE ComAct step consists in calling the CHOOSE&PREPAREALTERNATIVE ComAct component, followed by a call of the component TRY ComAct to execute the ComAct for the chosen alternative and the corresponding prepared message(s) (if this ComAct is possible for the message(s)). This is synthesized in symbolic form by the following definition: 7 TRYALTERNATIVE ComAct (subj, state) ¼ CHOOSE&PREPAREALTERNATIVE ComAct (subj, state) seq TRY ComAct (subj, state) The two components define the multiprocess character of S-BPM communication. Multiprocess communication means to communicate a bundle of mult(alt) >1 messages belonging to the chosen multialternative. Bundling means that to successfully execute a multiComAct a subject must successfully execute the ComAct for exactly the bundled messages that is mult(alt) many, without executing in between any other communication. Thus, executing a multiComAct is a multiround of single ComActs and appears as detailing one iteration step TRYALTERNATIVE ComAct of the TryRound described in Fig. 12.2. A further characteristics of a multiComAct in S-BPM consists in the requirement that (a) all relevant messages (those in the set MsgToBeHandled) must be prepared together before for each of them the execution of the ComAct-step is attempted and that (b) when the multiComAct fails-that is if the ComAct fails for at least one of the bundled messages-the information on which ComAct-executions were successful resp. unsuccessful is available so that in case of failure the procedure HANDLEMULTIROUNDFAIL ComAct for error handling and possibly some compensation can be called.
We define CHOOSE&PREPAREALTERNATIVE ComAct in Sect. 12.5.1 und TRY Send and TRY Receive in Sect. 12.5.2.

Selection and Preparation of Messages
A subject can choose a communication alternative among those possible in a state in a nondeterministic manner or following a priority scheme. We express this by abstract functions select Alt and priority which can be refined as soon as a concrete state and the selection scheme intended there become known.
For each chosen communication alternative, the corresponding message to be sent resp. the kind of the to be received message (in case of a multicommunication the elements of the set MsgToBeHandled) must be prepared. This is done by the component PREPAREMSG ComAct described below.
Additionally a MANAGEALTERNATIVEROUND-component must guarantee that (a) each possible communication alternative in Alternative (subj, state) is selected in each TryRound exactly once and that (b) in case of a multicommunication alternative the multiround is initialized. For (a) in each round, the static set Alternative (subj, state) is copied into a dynamic set RoundAlternative.
This description is synthesized in symbolic form by the following definition whose component PREPAREMSG )) Before sending a message, a subject will composeMsg from the relevant data, that is from the values of the underlying data structures, which are accessed via an abstract function msgData. Similarly in a given state, a receiver chooses one message kind out of those which are possible in this state for to be expected messages, using a selection function select MsgKind . The abstract functions used here represent the interface to the underlying data states and can be refined as soon as the data structures become known. We assume only that there are functions sender (msg), type (msg), and receiver (msg) to extract the indicated information from a message; thus, composeMsg has to insert this information. Similarly for expectedMsgKind and select MsgKind .
The preceding description defines the component PREPAREMSG Send and is symbolically synthesized as follows: PREPAREMSG

Sending and Receiving Messages
TRY Send is defined by the flowchart in Fig. 12.3, TRY Receive by the analogous only slightly different flowchart in Fig. 12.4. Both diagrams describe for multicommunication nodes the multiround of a TryRound-ComAct-step: once a communication alternative has been selected and the corresponding set MsgToBeHandled has been prepared, during the multiround successively for each m 2 MsgToBeHandled an attempt is made to send resp. receive m performing the steps described below. After concluding the ComAct for an m (with success or failure), the subject continues the multiround for the next available m 2 MsgToBeHandled; at the end of the multiround in case of failure of