Information Technology Reference
In-Depth Information
-
the function
p
M
:
Conf
M
→
(
VA
→
VA
) is defined by:
p
M
(
conf
)
σ
=
i
=1
I
(
conf
)
i
σ,
where
I
(
conf
)
σ
=
p
1
(
conf
1
)
σ
+
···
+
p
k
(
conf
k
)
σ
+
p
(
σ
r
+
σ
)
,
conf
=(
conf
1
,...,conf
k
,σ
r
)
,
and
d
is the depth of graph(
M
),
-
the function
out
M
:
Conf
M
×
(
i
→
V
)
→
(
o
→
V
) is defined by:
out
M
(
conf ,σ
i
)= (
p
M
(
conf
)
σ
i
)
|
o,
and
(
i
-
the function
next
M
:
Conf
M
×
→
V
)
→
Conf
M
is defined by:
next
M
(
conf ,σ
i
)=(
next
1
(
conf
1
,σ
i
)
,...,next
k
(
conf
k
,σ
i
)
, update
(
σ
r
,σ
))
,
where
conf
=(
conf
1
,...,conf
k
,σ
r
)and
σ
=
p
M
(
conf
)
σ
i
.
6
Representing Modules in Uppaal
In this section we will consider automated verification of modules. Since modules
basically are finite automata, there are many ways to address this problem. In
an initial study we experimented with using monadic second-order logics [6,7]
for expressing the semantics and using the MONA tool [10] for verification. For
the semantical part the experiment was promising, and it has the nice property
that second-order quantification can be used to express hiding and refinement
of modules can be expressed by implication. For the verification part we did,
however, only succeed with very small examples. The problem is that
n
second-
order variables are necessary to model an
n
-bit Gezel variable.
In the next experiments Uppaal [4] was used. Uppaal is a model-checking
tool based on timed automata [1]. Even though we have no real-time notions
in modules, there was several reasons for experimenting with Uppaal: In other
discrete models for embedded systems [5,9] Uppaal has proven to be a powerful
tool. Furthermore, a timed-automata based approach to verification of modules
would prepare for later real-time extensions.
6.1
Main Idea of the Uppaal Representation
In the Uppaal model of timed automata, a system consists of a parallel com-
position of
n
≥
1 timed automata. These timed automata can communicate by
synchronous communication over channels and by using shared variables. Tran-
sitions of a timed automaton can be guarded by a Boolean expression, and a
statement of a simple imperative programming language can be executed when
a transition is taken. Furthermore, real-valued clocks are used to express real-
time properties. For further introduction to Uppaal we refer to [4].
Search WWH ::
Custom Search