Information Technology Reference
In-Depth Information
In order to formalize quality constraints, we translate their EPPSL models into CTL-
formulas. Here, we differentiate between two kinds of models depending on the number
of control nodes they contain. Models which contain at most one control node are sim-
ple models. Models which contain more than one control node are complex models.
When we translate a simple or a complex model into a CTL-formula, we translate
the basic blocks: Actions, Guards, InitialNodes, and ActivityFinalNodes into the atomic
propositions: Actions labels, Guards texts, "Start", and "End" respectively. However,
the strategy for constructing the CTL-formula for a simple model differs from the strat-
egy for constructing it for a complex model. In the following, we explain the different
strategies.
5.1
The Translation Strategy for Simple Models
The translation of simple models depends on analyzing them to specific EPPSL pat-
terns, for which we provide a translation into CTL-formulas [21]. These patterns enable
all required combinations of EPPSL modeling elements, in order to cover all possible
semantics of quality constraints when the model contains at most one control node. For
example, we want to formalize
QC
6
which has to be verified on the business process
model in Fig. 1:
QC
6
:
"It is always true that checking the application data might be followed by re-
fusing the application, which is followed next by removing the application data from the
system"
.
First, we model
QC
6
with EPPSL (see Fig. 8), then we translate the model into a
CTL-formula by comparing it to the EPPSL patterns given by the translation tables,
which we provide in [21].
Fig. 8.
EPPSL quality constraint model
Due to lack of space, we show in Fig. 9 only a part of the translation tables ded-
icated for simple models, where
S
represents an EPPSL pattern, which is attached to
the element preceding
S
,and
S
∗
refers to the CTL-formula, to which
S
is translated.
C
represents a partial quality constraint model, and
C
∗
refers to the CTL-formula, to
which
C
is translated.
M
represents an EPPSL modeling element, and
M
∗
refers to the
CTL-formula, to which
M
is translated.
We can translate simple models from right to left or left to right. Here e.g., we trans-
late the model of
QC
6
from right to left as explained by Fig. 10. In Step 1, we translate
the Action "remove the application data from the system" to an atomic proposition rep-
resented by the Action label. In Steps 2, 3, 4, and 5, we divide the model into EPPSL
patterns provided by the translation table in Fig. 9. This enables us to translate each
pattern separately, until we reach the CTL-formula, which represents the whole model
in Step 5.
