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