Information Technology Reference
In-Depth Information
G
holds, modern decision procedures are able to generate a
proof
. In our setting,
a proof is a directed acyclic graph (
V, E,
), where
V
is a set of vertices,
E
is a
set of edges, and
is a labeling function. Each initial vertex
v
has in-degree 0
and
(
v
) is an axiom or a sub-conjunct of
G
. Each internal vertex has in-degree
m
,
m
1. The label of each inner node
w
is derived from the labels of its
predecessors
≥
(
w
).
The final vertex
u
has out-degree 0 and
(
u
) is the conclusion of the proof. SAT
solvers typically generate proofs that
{
v
1
,...,v
m
}
by means of a deduction rule
(
v
1
)
,...,
(
v
m
)
¬
G
is unsatisfiable, that is, the conclusion
is
F
.
Fixed-Points and Invariants.
For finite-state systems, iterating the transition
function until no new states are found is a viable verification technique, known
as fixed-point detection. This technique relies on an ecient symbolic repre-
sentation of sets of states such as binary decision diagrams [29]. The following
recursive equations are iterated until
S
i
=
S
i
+1
:
S
0
=
{
s
0
|
I
(
s
0
)
}
,
S
i
+1
=
S
i
∪{
s
i
+1
|
s
i
∈S
i
∧
R
(
s
i
,s
i
+1
)
}
(8)
Let
J
be a symbolic representation of the final
S
i
in this sequence. Then
J
is an
inductive invariant, i.e., it holds that
I
(
s
0
)
⇒
J
(
s
0
)
,
and
J
(
s
i
)
∧
R
(
s
i
,s
i
+1
)
⇒
J
(
s
i
+1
)
.
(9)
A popular technique to find invariants is the over-approximation of the set of
safe states by means of Craig interpolation [30].
5.2
Reusing Proofs and Invariants for Proving Unobservability
Proof Analysis.
The techniques presented in this section are based on work re-
cently presented by Purandare et al. [31]. Consider a system
M
and a mutated
system
M
o
in which all the mutations are introduced, but disabled using
F
∅
, i.e.
∀
f
i
.Thus,
M
and
M
o
are equivalent, i.e.
s
i
.o
=
s
i
.o
at all times. The equiv-
alence checking Formula (1) is unsatisfiable for all
k
. As stated in Section 5.1,
k
-induction is one possibility to prove equivalence of
M
and
M
o
.Let
T
be a set
of indices corresponding to all possible mutations (cf. Section 4.1). The formulae
that
k
-induction checks to establish equivalence of
M
and
M
o
are as follows:
i.
¬
k−
1
k−
1
k
I
(
s
0
)
R
(
s
i
,s
i
+1
)
f
j
s
i
.o
=
s
i
.o
equality of output
(10)
I
(
s
0
)
∧
R
(
s
i
,s
i
+1
)
∧
∧
∧
T
¬
∧
i
=0
i
=0
j
∈
i
=0
disable T
original model
mutated model
⎛
⎞
k
k
⎝
⎠
⇒
R
(
s
i
,s
i
+1
))
f
j
s
j
.o
=
s
j
.o
s
k
+1
.o
=
s
k
+1
.o
(
R
(
s
i
,s
i
+1
)
∧
∧
T
¬
∧
i
=0
j
∈
j
=0
(11)
