Information Technology Reference
In-Depth Information
7.4 Linking the Levels
Once two neighbouring levels of formal descriptions of real-time systems have
been given a semantics in the same semantic domain, here the Duration Calculus,
we can formally argue about correctness.
Consider a PLC-Automaton
A
and a collection of Constraint Diagrams
C
.
The semantics of
A
is given by a DC formula [[
A
]]
DC
and the semantics of
C
by
a DC formula [[
C
]]
DC
.Then
A
correctly renes
C
i [[
A
]]
DC
V
[[
C
]]
DC
.
Example 4.
Let
C
FES
be the collection of the ve Constraint Diagrams for-
malising the requirements for the lter
FES
in subsection 4.1 and
A
FES
the
PLC-Automaton of Fig. 5. Then we can prove:
If
"
PLC
"=
2then[
A
FES
]]
DC
V
[[
C
FES
]]
DC
.
"
Recall that
is the required reaction time of the lter to changes of the input
values and
A
FES
. It is typical
that correctness statements about PLC-Automata depend on certain constraints
on their cycle time. Using the continuous time domain
"
PLC
is the cycle time of the PLC-Automaton
Time
such constraints can
be conveniently stated and solved.
For the programming language ST we have not worked out any formal se-
mantics. It is clear that this is also desirable as it would enable us to prove
that ST programs correctly implement PLC-Automata and more generally ad-
dress the problem of compiler correctness. This is left for future work. A possible
approach can be found in [17].
8
Tool Support: Moby/PLC
Once such a semantic link based on logic has been well understood, tools can
be developed to support the design method. This has been done for the method
described in this paper by a tool called
[11]. It is implemented on
the basis of a C++ class library and emphasises graphic representations of the
objects. The architecture of
Moby/plc
Moby/plc
is displayed in Fig. 7; it consists of the
following components:
{
a graphic editor for PLC-Automata,
{
a simulator for networks of PLC-Automata,
{
a compiler generating code from PLC-Automata into the target language
ST for PLCs,
{
an algorithm for the static analysis of reaction times [7],
{
a synthesis algorithm for generating PLC-Automata from a subset of Dura-
tion Calculus that corresponds to DC implementables [8,28],
Search WWH ::
Custom Search