Information Technology Reference
In-Depth Information
cannot be controlled by a process but depends solely on the environment; it is
ignored in the semantic model used. The third phase, which executes in (at most)
outdelay
2
time units, is concerned with some operation after the communication
commenced.
The time
E
1
+
outdelay
1
+8 spent by the code before the communicated value
becomes available to the environment cannot be handed over to the successor as
the communication is visible to the environment. Together with the time
L
to
be absorbed from the predecessor it poses a constraint on time bounds that can
be guaranteed for the output statement. This is expressed by the condition on
E
.Thetime
outdelay
2
spent after the communication takes place, on the other
hand, is handed over to the sequential successor for absorption via parameter
R
.
Let us nally have a look at the timed version of Theorem 3.
Theorem 7 (Sequential composition translation).
Suppose
CS
0
(
stat
1
;m
1
;;L
1
;R
1
;E
1
)
,
CS
0
(
stat
2
;m
2
;;L
2
;R
2
;E
2
)
,and
R
1
L
2
.
CS
0
(
seq
(
stat
1
;
Then
stat
2
)
;m
1
m
2
;;L
1
;R
2
;E
1
+
E
2
)
.
m
2
for the second component
stat
2
must be able to absorb at least the excess time
R
1
L
2
expresses that the code
Here, the premise
R
1
handed over from the
rst component. Note that we can assert for a sequential composition the sum
of time bounds for its components.
From a collection of such theorems that describe construction of correct code
for each operator of the source language we have developed a code generator
written in the functional language Standard ML [30]. By adding a frontend, we
have constructed a prototypical compiler [36].
This concludes this overview on the modular veried design of code gener-
ators. The modularity of the approach facilitates the construction of code gen-
erators and assists rigorous control procedures because it allows to split both
tasks into relatively small, independent sub-tasks. Moreover, it enables reuse.
The derived views to the Transputer, e.g., can be exploited for dierent source
languages or even used when verifying boot programs or operating systems. To
use some form of renement as underlying notion of correctness instead of se-
mantic equivalence allows a proper treatment of under-specication in the target
and the source language, which allows, e.g., to give a proper meaning to unini-
tialized variables. Moreover it accommodates modularization. Like the work at
CLI (Computational Logic Inc.) on the `small stack' [7] we have put emphasis
on consistent interfaces to higher and lower levels of abstraction.
3
Synthesis of Embedded Real-Time Controllers
We will now turn to the problem of directly synthesizing real-time embedded
controllers from metric-time temporal logic specications. In comparison to im-
perative programming languages, such logics provide a very abstract means of
specifying what the system should do rather than saying how to achieve this.
Thus, using such logics as source languages for compilation or synthesis methods
for embedded controllers would be desirable. This is particularly true for those
Search WWH ::
Custom Search