Information Technology Reference
In-Depth Information
Fig. 6.
EPPSL modeling elements for logical relationships
Fig. 6 shows the notation of the EPPSL modeling elements for logical relationships.
The "Join/ForkNodes" and "Decision/MergeNodes" are the same control nodes used
by UML 2.0 Activity Diagrams. The "Not" and "Connector" elements are new classes
defined by EPPSL.
To give an example for using the logical relationships modeling elements, we assume
that we want to verify
QC
5
on the business process model in Fig. 1.
QC
5
:
"If there exists a possibility to make an interview, then there exists no possibility
to accept the application online"
.
The EPPSL model in Fig. 7 models
QC
5
. It includes two EPPSL models for two par-
tial quality constraints, which are temporally not related. This means that each one of
them must be checked separately on the business process. For this reason, we separate
each one in a ConstraintContainer. The first model states that there exists a possibility
to make an interview after starting the process. The second model states that there exists
no possibility to accept the application online after starting the process. The Constraint-
Containers are linked with a Connector, which means that the partial quality constraint
represented by the first model must imply the partial quality constraint represented by
the second model.
Fig. 7.
EPPSL quality constraint model
5
Translation of EPPSL Models into CTL-Formulas
The Computation Tree Logic (CTL) [6] views the time as a tree. It considers all different
paths, allowing the future to be non-deterministic. CTL-formulas are based on a set
of atomic propositions (statements which truth value may change over time), logical
connectives (
), temporal operators (
X
:Next,
F
: Eventually,
U
: Until,
G
:
Globally), and path quantifiers (
A
: On all paths,
E
: On at least one path). Whenever
there is a temporal operator in a CTL-formula, a path quantifier must precede it. For
example, if
¬
,
∧
,
∨
,
⇒
ψ
is an atomic proposition, then
AX
ψ
is a CTL-formula, which states that,
On all paths,
ψ
holds next.
