Information Technology Reference
In-Depth Information
another action, may be allowed to happen solely if a certain result, e.g., the object
has been set to 'high', occurred. Both, actions and results, are represented by Boolean
propositions at each state. For instance, proposition
ra
being 'true' at a state
s
i
means
that the action, i.e., execution of activity 'risk analysis', has happened at state
s
i
.In
contrast, proposition
ra
being 'false' at state
s
i
means that the action did not happen at
state
s
i
. Given a trace
σ
:
s
0
,s
1
,...,s
n
, we write
p
∈
s
i
to indicate that proposition
p
is true in state
s
i
,for
0
≤
i
≤
n
and
p
∈
σ
if there is a state
s
i
in
σ
where
p
∈
s
i
,for
some
n
.
We represent an execution sequence as a linear sequence of states where states are
labelled with both actions and results, and (unlabelled) edges between states represent
the temporal ordering in the sequence. Hence, we rely on Linear Temporal Logic (LTL)
in order to formulate statements about traces.
0
≤
i
≤
2.2
Linear Temporal Logic
Linear Temporal Logic (LTL) [20] is a logic specifically designed for expressing and
reasoning about properties of linear sequences of states. The formulae of LTL are built
from atomic propositions using the connectives of
(im-
plication), and the following temporal connectives:
X
(next),
F
(eventually),
G
(always),
U
(until) and
B
(before). The latter are interpreted as follows:
X
ϕ
:
in the neXt state,
ϕ
holds
F
ϕ
:
there is some state either now or in the Future where
ϕ
holds
G
ϕ
:
in every state Globally from now on,
ϕ
holds
ϕ
U
ψ
:
there is some state, either now or in the future, where
ψ
holds, and
ϕ
holds in
every state from now Until that state
ϕ
B
ψ
:
Before
ψ
holds, if it ever does,
ϕ
must hold.
We apply LTL to encode compliance requirements. Hence, we obtain a set of formulae
Γ
expressing the constraints to which compliant traces have to conform.
∨
(or),
∧
(and),
¬
(not) and
⇒
2.3
Finding All LTL-Models of a Given LTL Formula
Given a collection of compliance requirements expressed as a set
Γ
of LTL-formulae,
we seek to find a behavioral model that captures all
formula-models
, i.e., traces in our
setting, which satisfy
Γ
. That is, such a model describes all linear sequences of states
s
0
,s
1
,...,s
n
such that
Γ
is true at
s
0
.Since
Γ
may contain
eventualities
,suchas
X
ϕ
or
ψ
1
U
ψ
2
, ensuring that
Γ
is true at
s
0
may require us to ensure that
ϕ
is true at
s
1
or
ψ
2
is true eventually at some state
s
i
with
n
. In contrast to model checking [7]
we are not given a single trace, but construct all traces satisfying the given constraints.
The first step is to determine whether the constraints are satisfiable. If not, the spec-
ification is erroneous since no trace can conform to the given constraints. The second
step is the creation of the behavioral model that describes
all
traces.
For both steps, we use a tableaux-based method introduced in [24,23]. In essence,
this approach works as follows. We start by creating a root node containing
Γ
and
proceed in two phases. First, a finite (cyclic) graph of tableau nodes is created by ap-
plying tableau-expansion rules that capture the semantics of LTL and by pruning nodes
containing local contradictions [24]. Second, once the graph is complete a reachability
0
≤
i
≤
