Services as a Paradigm of Computation - Formal Methods and Hybrid Real-Time Systems - page 530

coin

“tea!”

“coffee!“

beverage

Fig. 2. Example of an oWFN: A beverage service A

The pragmatic idea of oWFNs is obvious: An oWFN N describes a set of
runs, starting at the initial marking.
According to the above described pragmatic idea of oWFNs, termination is a
crucial issue. An isolated oWFN rarely terminates; usually a partner is required,
such that the composed system would terminate. We consider the weakest version
of termination in the sequel: An oWFN N is weakly terminating if each sequence
m 0

t 1
−→

t 2
−→ ... t k

t i
−→ m i ( i =1 ,...,k )isaprefixofarun

of N (i.e. can be extended to eventually reach a final state).
A sequence of steps may fail to be extensible to a run due to a wrong number
of tokens at input or output places.
We occasionally want to abstract from input and output and concentrate on
the inner subnet :
For an oWFN N ,theset

m 1 −→ m k of steps m i− 1

I = def in ∪ out

is the interface of N ,and

J = def P \ I

is the set of inner places of N .Furthermore,

inner ( N )=( J, T, F ,m 0 ,Ω )
is the inner subnet of N , generated by the restriction to the inner places of N ,
the transitions of N , and the corresponding restriction of F, m 0 and Ω to J and
T . As an example, Fig. 3 shows the inner subnet of the oWFN in Fig. 2.
N is apparently ill designed in case inner ( N ) is not weakly terminating.
Historically, the term “open Workflow Nets” has been derived from workflow
nets [15]. A workflow net is a formal model of the process logic of a workflow.
Conceptually, a service extends workflows with an explicit interface to enable