Information Technology Reference
In-Depth Information
Theorem 3.
Given a system
P
then:
• P
satisfies SNNI iff
α
T
◦
α
low
(
{| P |}
)=
α
T
◦
α
low
◦
α
L
(
{| P |}
)
;
• P
satisfies BNDC iff
∀Π.
(
α
B
◦
α
L
)
◦
α
INT
(
{| P ||Π|}
)=
α
B
◦
α
L
(
{| P ||Π|}
)
.
3.3
GANI in Real-Time Systems
Let
A
be a timed automaton [1],
{| A|}
the corresponding computational tree
def
=
L
α
T
(
{| A|}
semantics, and
) the corresponding timed accepted language, i.e.,
the sequence of all the computational traces of states
σ, t
σ
,where
is an action
t
executed at the time
. In [2] a notion of non-interference for timed automata is
introduced. Given a natural number
n
, the authors say that high-level actions
do not interfere with the system, by considering minimum delay
n
, if the system
behaviour in absence of high-level actions is equivalent to the system behaviour,
observed on low-level actions only, when high-level actions can occur with a
delay between them greater than
n
.Let
Σ
be the alphabet of actions of
A
.We
suppose that
is partitioned into two disjoint sets of actions
H
and
L
:
H
is the
set of the high-level actions, while
L
is the set of the low-level ones. Consider the
following languages:
Σ
=
∀σ
i
,t
i
∈σ, t .σ
i
∈
L
def
L|
L
σ, t∈L
∃σ, t∈L
such that
w
is the projection of
σ, t
σ ∈
L
L/
H
de
=
on the pairs
σ, t
w
∀σ
i
,t
i
, σ
j
,t
j
∈σ, t .i
=
j,
L
H
def
=
σ, t∈L
σ
i
,σ
j
∈
H
⇒ t
i
− t
j
|≥n
So,
L|
L
avoids high-level actions, i.e., it takes only the traces of the system that
make only low-level actions. On the other hand,
L/
H
hides all the high-level
actions, i.e., it executes them and then it hides them. Finally,
L
H
selects only
those traces where the high-level actions are distant at least
n
.Thenin[2]a
L
H
/
H
=
system is said to be
n-non-interfering
iff
L|
L
.
Consider the example below [2]. This timed automaton have
L
=
{
begin-c,end-c
}
and
H
=
{
cloche,reset
}
. There is only one possible trace of only low-level actions:
begin-c
,
2
end-c
,
4
...
begin-c
,
2+4
i
end-c
,
4+4
i ...
If more than one cloche
action is executed and
the time elapsed between
them is less than 1, then
it is possible to execute
the action reset, which
can change the moment
of the execution of begin-
c, and therefore in this
case we have an interfer-
ence.
x
0
= 2,begin-c,
{}
x
0
= 1,cloche,
{x
1
}
s
1
s
2
s
0
x
1
=1
,,{}
x
0
= 4,end-c,
{x
0
}
x
0
≤
2
x
1
<
1,cloche,
{x
1
}
, {}
x
0
>
2
reset,
{x
0
}
s
3
x
1
<
1,cloche,
{x
1
}
