Information Technology Reference
In-Depth Information
The C program works as follows. If h2
c
,theclockofFB
c
, has the value
T
,
a new value for FB is read and assigned to the variable N
c
.Ifh2
c
is
F
,N
c
gets
the value ZN
c
−
1. In both cases the updated value of N is output (at
l
4
)and
also copied into ZN
c
, for reference in the next step .
A computation of this program is given below. We skip intermediate states
and consider complete iterations of the while loop. The notation
X
:
is used
X
to denote that variable
has an arbitrary value.
8
:
9
;
8
:
9
;
8
:
9
;
8
:
9
;
8
:
9
;
8
:
9
;
FB :
FB : 3
N: 3
ZN : 3
h1 :
FB : 3
N: 2
ZN : 2
h1 :
FB : 3
N: 1
ZN : 1
h1 :
FB : 5
N: 5
ZN : 5
h1 :
FB : 5
N: 4
ZN : 4
h1 :
ZN : 1
h1 :
N:
!
!
!
!
!
!
T
T
T
T
T
h2 :
h2 :
T
h2 :
F
h2 :
F
h2 :
T
h2 :
F
:
l
0
:
l
0
:
l
0
:
l
0
:
l
0
:
l
0
Taking into account that h1
c
is the clock of N
c
and that h2
c
is the clock
of FB
c
, we have an accurate state correspondence between the computation of
the
program and the computation of the C-code, when we restrict our
observations to subsequent visits at location
Signal
l
0
.
This state correspondence is a general pattern for programs generated by
the
sacres
compiler. Intuitively, the generated C-code correctly implements the
original
Signal
program if the sequence of states obtained at the designated
control location
l
0
corresponds to a possible sequence of states in the abstract
system.
In the rest of the paper, we show how this approach can be formalized and
yield a fully automatic translation validation process.
3 Computational Model and Semantics of
Signal
In order to present the formal semantics of
Signal
we introduce a variant of
synchronous transition systems
(
sts
)[20].
sts
is the computational model of our
translation validation approach.
Let
V
s
V
be a set of typed variables. A
state
over
is a type-consistent
interpretation of the variables in
V
. Let
V
denote the set of all states over
V
.
A
synchronous transition system
A
=(
V;;
) consists of a nite set
V
of typed
variables, a satisable assertion
characterizing the initial states of system
A
,
V;V
0
), which relates a state
and a transition relation
. This is an assertion
(
s
0
2
V
s 2
V
to its possible successors
by referring to both unprimed and
primed versions of variables in
V
. Unprimed variables are interpreted according
s
0
. To the state space of an
to
we refer as
A
. We will also use the term \system" to abbreviate \synchronous transition
system". Some of the variables in
s
, primed variables according to
sts
A
are identied as
volatile
while the others are
identied as
persistent
. Volatile variables represent flows of
V
Signal
programs,
thus their domains contain the designated element
?
to indicate absence of the
respective flow.
Search WWH ::
Custom Search