Information Technology Reference
In-Depth Information
GEAR basically uses the
Computation Tree Logic
(CTL) [70, Chapter 3]
to formulate model checking constraints. CTL is a temporal, branching time
logic designed to reason about models represented as directed graphs, and
whose syntax can be described by the following BNF:
φ
::=
p
|¬
φ
|
φ
∨
φ
|
φ
∧
φ
|
AX
(
φ
)
|
EX
(
φ
)
|
AF
(
φ
)
|
EF
(
φ
)
|
AG
(
φ
)
|
EG
(
φ
)
|
EWU
(
φ, φ
)
Thus, in addition to the operations and operands known from propositional
logic, it comprises the modalities
AX
,
EX
,
AF
,
EF
,
AG
,
EG
,
ASU
,
ESU
,
AWU
and
EWU
.The
A
sand
E
sare
path-quantifiers
, providing a universal
(
A
)orexistential(
E
) quantification over the paths beginning at a state.
X
,
F
,
G
,and
SU
and
WU
express
linear-time modalities
for the path.
X
expresses
that
φ
must be valid in the
next
state,
F
specifies that
φ
must hold
finally
,
and
G
requires
φ
to hold
generally
(always).
SU
(
strong until
) expresses that
φ
1
has to be valid until
φ
2
, with requiring to
φ
2
to hold finally. The
weak until
modality (
WU
) also requires
φ
1
to be valid until
φ
2
, but does not require
φ
2
to hold if
φ
1
holds infinitely. A formal definition of the semantics can be
found, for instance, in [70, Chapter 3] or [228].
Model checking in terms of CTL works on the Kripke Structure portion of
the SLGs. In order to enable the formulation of model checking constraints
with respect to particular branches, GEAR can also interpret the
box
and
diamond
operators known from Hennessy-Milner logic (HML) [130]:
[
Trans
]
φ
ASU
(
φ, φ
)
|
ESU
(
φ, φ
)
|
AWU
(
φ, φ
)
|
φ
where
Trans
is a (possibly empty) set of labeled transitions (branches). The
box operator expresses that
φ
must hold for all successors of a particular state
that are reachable via one of the branches in
Trans
(universal quantification).
Analogously, the diamond operator requires
φ
to hold for at least one
Trans
-
successor (existential quantification).
GEAR extends these variants of CTL and HML further and includes addi-
tional overlined modalities that represent a backward view, that is, consider
the paths that end at a given state. As an example, the formula:
|
Trans
AG
(
φ
)
is fulfilled for all states where
φ
holds globally on all incoming paths.
Moreover, GEAR offers a variety of macros that provide composite opera-
tors or access to jABC-specific functionality.
2.2.2 Monitoring of User-Level Workflow
Constraints
As detailed above, the GEAR model checking plugin allows for the global and
continuous evaluation of (modal or temporal logic) constraints on the work-
flow model under development. This facilitates a constraint-guarded workflow
Search WWH ::
Custom Search