Information Technology Reference
In-Depth Information
::= te
j:j
(
^
)
j
<
c
>
j
G
(
)
j
(
U
)
where
te
represents a SIB constraint formulated as taxonomy expression, and
c
a possible condition.
In the IN-application, SLTL formulas are interpreted over the set of all
legal call
flows
, i.e. alternating sequences of SIBs and conditions
6
which start and end with
SIBs. The semantics of SLTL formulas is now intuitively dened as follows:
7
{
te
is satised by every call flow whose rst element (a SIB) satises the tax-
onomy expression
te
.
{
Negation
:
and conjunction
^
are interpreted in the usual fashion.
{
Next-time
operator
<>
:
<
c
>
is satised by all call flows whose second element (the rst condition)
satises
c
and whose
continuation
8
satises
. In particular,
<
tt
>
is sat-
ised by every call flow whose continuation satises
.
{
Generally
operator
G
:
is satised for every sux
9
.
G
(
) requires that
{
Until
operator
U
:
(
holds at all BBs of the sequence,
until a position is reached where the corresponding continuation satises the
property
U
Ψ
) expresses that the property
Ψ
.Notethat
U
Ψ
guarantees that the property
Ψ
holds eventually
(strong until).
The denitions of continuation and sux may seem complicated at rst. How-
ever, thinking in terms of paths within a flow graph claries the situation: a
subpath always starts with a node (SIB) again.
The interpretation of the logic over service models is dened path-wise: a
service model satises a SLTL formula if all its paths do.
The introduction of
derived operators
supports a modular and intuitive for-
mulation of complex properties. Convenient are the dual operators
False
:
=
df
:
tt
Disjunction
:
_ Ψ
=
df
:
(
: ^:Ψ
)
Box
:
[
c
]
=
df
: <c>
(
:
)
Eventually
:
F
(
)=
df
:
G
(
:
)=
tt
U
)
The following two simple examples illustrate typical loose sequencing constraints
which can be conveniently specied in SLTL:
6
The absence of a condition is identied with the condition
true
.
7
A formal denition of the semantics can be found in [19].
8
This continuation is simply the call flow starting from the second SIB.
9
A sux of a call flow is any subsequence arising from deleting the rst 2n elements
(n any natural number).
Search WWH ::
Custom Search