Information Technology Reference
In-Depth Information
5.2
The Translation Strategies for Complex Models
Logical relationships may link actions and guards, or may link partial quality constraints
with respect to the basic assumptions defined in [21]. For this purpose, we define two
different translation strategies for complex models. The first one is used when more than
one control node link Actions and Guards (e.g. the model in Fig. 11), and the second
one is used when more than one control node link ConstraintContainers (e.g. the model
in Fig. 13).
Strategy 1: Given an EPPSL complex model, e.g. the complex model of QC 7 in Fig.
11, which we want to verify on the business process model in Fig. 1:
QC 7 : "Receiving an application is always followed by making an interview or refus-
ing the application and remove the application data from the system" .
l 4
l 3
l 2
l 1
Fig. 11. Example of a complex model
We translate the model in Fig. 11 by applying the following steps:
1. We divide the model into levels numbering them in the opposite direction of the
temporal relationships. In Fig. 11, we have 4 levels.
2. We assign a variable name to each temporal relationship followed and preceded
directly by a control node. In Fig. 11, we have one variable X .
3. When a control node is preceded directly only by a variable with no assigned value
and followed directly by temporal relationships attached only to Actions or Guards,
then the node has to be translated according to the translation table dedicated for
control nodes preceded by variables [21] (due to lack of space, we present only
a part of it in Fig. 12) and the resulting CTL-formula is assigned to the variable.
According to the table in Fig. 12, we translate the ForkNode on Level 2 in Fig. 11,
and we assign its formula to X :
X: ( AF (refuse the application)
AF (remove the application data from the system))
4. When a control node is followed directly only by a variable with no assigned value
and preceded directly by temporal relationships attached only to Actions or Guards,
then the node has to be translated according to the translation table of control nodes
followed by variables [21], and the resulting CTL-formula is assigned to the vari-
able. Fig. 11 does not encounter this case.
Search WWH ::




Custom Search