Information Technology Reference
In-Depth Information
Fig. 12.
Example of translating control nodes preceded by a variable into CTL-formulas
5. We translate the control nodes of the model if they are yet not translated starting
at the second level (the first level always includes Actions or Guards which are
translated into atomic propositions). The variables which are yet not assigned a
CTL-formula and followed directly by control nodes, which are in turn directly
followed by Actions, Guards or variables already assigned a CTL-formula in terms
of Actions or Guards, are assigned the CTL-formula to which the control node is
translated according to the translation table of control nodes preceded by variables
[21]. Fig. 11 does not encounter this case.
If we reach a control node, which all incoming and outgoing temporal rela-
tionships are attached to Actions, Guards, or variables with assigned values, we
translate it according to the translation tables of control nodes dedicated for simple
models [21]. For example, we translate the DecisionNode on Level 3 in Fig. 11
depending on the first EPPSL Pattern in Fig. 9:
AG
(receive application
→
(
AF
(X)
∨
AF
(make an interview)))
We substitute
X
by its value:
AG
(receive application
→
∧
(
AF
((
AF
(refuse the application)
AF
(remove the ap-
∨
plication data from the system)))
AF
(make an interview)))
The previous CTL-formula represents the whole complex model in Fig. 11.
Strategy 2:
Given an EPPSL complex model, e.g. the complex model of
QC
8
in Fig. 13,
which we want to verify on the business process model in Fig. 1:
QC
8
:
"If there exists a possibility to make an interview, then there exists no possibility
to accept the application online and there exists a possibility to make an interview per
phone or there exists a possibility to make an interview per Internet"
.
We translate the model in Fig. 13 by applying the following steps:
1. Each control node may have either multiple incoming connectors or multiple out-
going connectors. In both cases, we combine the control node with its multiple
connectors and their attached ConstraintContainers in one ConstraintContainer. For
example, in Fig. 13, we apply this rule on the DecisionNode and the ForkNode re-
sulting in two new ConstraintContainers as shown in Fig. 14.
2. We start to translate the partial quality constraint models which do not include
ConstraintContainers. For example, in Fig. 14, we translate (1), (2), (3), and (4)
depending on the EPPSL patterns in Fig. 9:
(1):
Start
→
EF
(make an interview)
(2):
Start
→¬
EF
(accept the application online)
