418
R. Khennaoui and N. Belala
Disabling. During the activity execution, it is possible to indicate its failure
with the disabling operator [>. A [> B means activity A may be disabled by
activity B which interrupts the main flow and uses stop instead of exit.
Parallelism (general case). A |[L]| B means if the process (activity A) is
ready to execute some action at one of the synchronization gates, it is forced,
in the absence of alternative actions, to wait until the process (activity B)
offers the same action.
Full Synchronization. A B means that if L = ∂, the two composed activities
are forced to execute in complete synchronicity.
Pure Interleaving. If L = ∅, the absence of synchronization leads to the
absence of interaction points among processes, this is achieved through the
interleaving operator ‘|||’.
2.2 Contextual Planning System of the Workflow
In order to illustrate the concept of the formal design of workflows with
the contextual information, the contextual planning system is built from an
Ag-LOTOS specification using the rules in Table 1.
Table 1. The semantic rules.
Action:
ws
a
− → ws
a ∈ Act
(ws, l)
a
− → (ws , l)
Mobility:
ws
move(l
)
−−−−−→ ws
(l = l
)
(ws, l)
move(l )
−−−−−→ (ws , l )
Communication: (a)
ws
x!(u)
− −− → ws
(u ∈ U)
(ws, l)
x!(u)
− −− → (ws , l)
(b)
ws
x?(u)
−−−→ ws
(u ∈ U)
(ws, l)
x?(u)
−−−→ (ws , l)
The Contextual Planning System of the Workflow (CPSw) based on CPS
[22] takes into account two types of information: workflow planning state ws and
locality l. Table 1 shows the operational semantic rules that define the possible
planning state changes for the workflow. From an initial planning state (ws 0 , l),
we apply these rules to produce the CPSw. The contextual planning system
CPSw is a labeled Kripke structure (S, s 0 , T r, L) where S is the set of contextual
planning workflow states, s 0 = (ws 0 , l) ∈ S is the initial planning state of the
workflow, T r ⊆ S × ∂ ∪ {T } × S is the set of transitions which are denoted
s
a
− → s
, and L : S → → is the location labeling function.
3 Case Study
In this paper, we target on context-aware workflow models for ubiquitous company. Let there be an enterprise with several helpdesk employees associated with
smart badges that provide the system with spatial information at each moment.
R. Khennaoui and N. Belala
Disabling. During the activity execution, it is possible to indicate its failure
with the disabling operator [>. A [> B means activity A may be disabled by
activity B which interrupts the main flow and uses stop instead of exit.
Parallelism (general case). A |[L]| B means if the process (activity A) is
ready to execute some action at one of the synchronization gates, it is forced,
in the absence of alternative actions, to wait until the process (activity B)
offers the same action.
Full Synchronization. A B means that if L = ∂, the two composed activities
are forced to execute in complete synchronicity.
Pure Interleaving. If L = ∅, the absence of synchronization leads to the
absence of interaction points among processes, this is achieved through the
interleaving operator ‘|||’.
2.2 Contextual Planning System of the Workflow
In order to illustrate the concept of the formal design of workflows with
the contextual information, the contextual planning system is built from an
Ag-LOTOS specification using the rules in Table 1.
Table 1. The semantic rules.
Action:
ws
a
− → ws
a ∈ Act
(ws, l)
a
− → (ws , l)
Mobility:
ws
move(l
)
−−−−−→ ws
(l = l
)
(ws, l)
move(l )
−−−−−→ (ws , l )
Communication: (a)
ws
x!(u)
− −− → ws
(u ∈ U)
(ws, l)
x!(u)
− −− → (ws , l)
(b)
ws
x?(u)
−−−→ ws
(u ∈ U)
(ws, l)
x?(u)
−−−→ (ws , l)
The Contextual Planning System of the Workflow (CPSw) based on CPS
[22] takes into account two types of information: workflow planning state ws and
locality l. Table 1 shows the operational semantic rules that define the possible
planning state changes for the workflow. From an initial planning state (ws 0 , l),
we apply these rules to produce the CPSw. The contextual planning system
CPSw is a labeled Kripke structure (S, s 0 , T r, L) where S is the set of contextual
planning workflow states, s 0 = (ws 0 , l) ∈ S is the initial planning state of the
workflow, T r ⊆ S × ∂ ∪ {T } × S is the set of transitions which are denoted
s
a
− → s
, and L : S → → is the location labeling function.
3 Case Study
In this paper, we target on context-aware workflow models for ubiquitous company. Let there be an enterprise with several helpdesk employees associated with
smart badges that provide the system with spatial information at each moment.