close

Вход

Забыли?

вход по аккаунту

ПОСЛЕДНЯЯ НОВОСТЬ;pdf

код для вставкиСкачать
Realizing Real-Time Systems from Synchronous Language
Specifications
R. K. Shyamasundar
J.V. Aghav
School of Technology & Computer Science
Tata Institute of Fundamental Research
Homi Bhabha Road, Mumbai 400 005, India
School of Technology & Computer Science
Tata Institute of Fundamental Research
Homi Bhabha Road, Mumbai 400 005, India
[email protected]
[email protected]
ABSTRACT
Synhronous languages speify reations of the reative/realtime systems to its environment within the language. This
makes it easier to validate and verify the systems relative
to the assumptions and notions of simultaneity. However,
onrete embedding of the ode makes it neessary to predit time for reations of the underlying run-time systems
and the sensors so that the strit notion of simultaneity an
be relaxed keeping the logial orretness intat. Further,
for hard real-time systems, there is a need for referring to
lok times. In this paper, we desribe a method that uses
timed annotations for Esterel programs that makes it possible to predit the timing onstraints on run-time system,
the sensors and lok times and validate the onrete realization relative to time-annotated Esterel speiations.
Using suh time annotations, it is possible to establish that
the onrete implementation is indeed a orret realization
of the abstrat system speied in annotated Esterel. Further, the method establishes time onstraints to be satised
by the onrete arhitetures for realizing the logial speiation of the system. We shall illustrate the design and
implementation of the tool using some of the existing ode
generation tools of the Esterel environment. Furthermore,
the method an also be used for arriving at sheduling onstraints on the underlying asynhronous tasks.
1. INTRODUCTION
There have been a variety of programming languages for
the design of real-time systems. Various models and logis
[?℄ employed to build real time systems and their abstration to FSA for purposes of veriation are given in [?℄.
In real-time languages, onstruts allow us to speify and
Work done under grant from the Indo-Frenh Centre for
the Promotion of Advaned Researh, New Delhi, under the
projet 2202-1 Formal speiation and veriation of hybrid
and reative systems.
realize timing onstraints of the implemented systems. Synhronous languages [?, ?℄ are another important family of
languages that have been widely used for programming reative systems. In these languages, the following logial assumptions (often referred to as perfet synhrony) are made
(i) The program produes its outputs in no observable time,
(ii) Conurrent statements evolve in a tightly oupled way,
and (iii) Communiation is done by instantaneous broadasting, the reeiver reeiving it exatly at the time it is
sent. Thus, in the ontext of a synhronous language, several variables are allowed to hange their values in a single
step (i.e. simultaneity is possible). However, suh things are
not possible in an asynhronous setting on a given arhiteture. While assumptions suh as innitely fast mahines are
useful to verify anomalies/paradoxes in the speiations at
the logial level, there is a need to relax the requirement
of simultaneity for the objet ode generated running on
real mahines. The standard aeptable relaxation is that
we divide the time line into many small intervals and all the
events that our in the same interval (or instant in the ontext of synhronous languages) are onsidered simultaneous.
Obviously there is a need for ensuring that these assumptions are met. Furthermore, in an atual implementation
there will be need to refer to lok-time. Sine there is no
lok in Esterel all these signals have to ome from the
environment. Designing real-time systems with synhronous
tehnologies, follow the two-step methodology given below:
1. Establish the logial orretness (following the lassial
Compile-simulate-verify yle in Esterel ).
2. Establish the satisfation of time onstraints are met
taking into aount the synhrony/simultaneity and
the lok-time referenes; signals/events happening in
the same instant are treated to be simultaneous.
The general methodology of Esterel validation is depited
in Figure ??.
In this paper, we shall propose a method and the design of
a tool for (i) speifying timing onstraints on the signals in
the environment and for exeution of ode snippets, in Esterel speiations, synhrony/simultaneity assumptions,
and (ii) a method and a tool for establishing that the implementation is a realization of the speiation on the given
arhiteture. Our method is based on annotating Esterel
programs using the notation alled TimeC explored in [?℄ in
the ontext of verifying onstraints in ompilers meant for
ILP proessors and deriving the global onstraints for the
System concepts
Arrive at ESTEREL
Specifications
Compile-Simulate-debug
Verify Logical Correctness
M0:
M1:
M2:
Verify Timing Assumptions
Figure 1: Methodology of Esterel ode Validation
satisfation of the synhrony hypothesis. One of the novel
features of, TimeC, is that the language is independent of
the base language being used to develop embedded appliations. The main ontributions of the paper are:
1. Speifying time onstraints using TimeC in synhronous
languages suh as Esterel with referene to the signal
environment that may inlude loks.
2. A method of relating timing onstraints on the signal
environment of Esterel for the satisfation of synhrony assumptions. Also, from the method it is possible to derive sheduling onstraints of the external
asynhronous tasks used for meeting the timing onstraints of the signal environment.
3. The struture of a tool for the proposed method of
validating the timing onstraints relative to the synhronous onstraints.
In the following, we shall give an overview of the method.
For lak of spae, we shall only be skething the method and
the interested reader is referred to the full paper.
2. AN INFORMAL OVERVIEW
Our approah is based on using timing annotations in the
original Esterel program and deriving timing onstraints
for the satisfation of the synhrony hypothesis.. The method
essentially onsists of
(i) Annotating
Esterel
fragments with the onstraints,
(ii) Embed the timing onstraints in the program through
logial (ghost) signals without hanging the timing
properties of the original program,
(iii) Obtain the automata whose transitions onsists of labels onsisting of the original signals of the program
and the additional logial signals introdued,
(iv) Derive the timing onstraints for eah of the transitions
for the satisfation of the synhrony hypothesis, and
(v) Verify the validity of the timing onstraints.
An overview of the various steps of the method is informally desribed below using the fragment of the Esterel
program used for ontrolling the path of a boat against a
given diretion as shown in Figure ??.
M3:
M4:
M5:
M6:
M7:
M8:
module loseness:
funtion lose enough():integer;
funtion reahed p():integer;
output suppress;
output terminate;
output o ontinue;
trap term in
loop
if (lose enough() = 1)
then emit suppress
else nothing
end; %if
if (reahed p() = 1)
then emit terminate;exit term;
else nothing
end; % if
await tik;
end; % loop
end; % trap
.
Figure 2: Esterel Fragment with Loation Labels
No.
1.
2.
3.
4.
5.
6.
Constraint
time(M2) - time (M1)
10 units
time(M3) - time (M1)
6 units
time(M5) - time (M4)
8 units
time(M6) - time (M4)
4 units
time(M8) - time (M7)
? indeterminate
time(M0) - time (M1)
= 3 units
Comments
time for testing &
then-branh exeution
time for testing &
else-branh exeution
time for testing &
then-branh exeution
time for testing &
else-branh exeution
awaiting for an
external event
time to get into
next iteration
Table 1: Timing Constraints
Various time onstraints
suh as maximal, minimal, exat [?℄ an be speied. The
timing onstraints are speied as follows:
1. Even though the input and output signals are assumed
to be instantaneous in Esterel atuators ause delay
in the ompletion of reation. The time onstraint
to be satised by any onrete implementation an be
speied by plaing markers as in TimeC [?℄ at various
loations of the ode.
Speifying Timing Constraints:
2. Now the time onstraints at the respetive loations
are to be dened. For the fragment of the ode shown
in Fig. ??, markers have been shown as labels at various points of ode and the onstraints to be satised
are shown in Table ??. Here, the prediate time(`) indiates the global time when the ontrol reahes label
`.
Note: It may be noted that onstraints illustrated in (5) of
Table ?? an also be used for speifying expliit lok times
relative to the signals used. Some of these details are not
further disussed here for want of spae.
Deriving Global Timing Constraints: Having speied
the arhitetural timing onstraints, we have to arrive at
of referene and speifying onstraints, we use \begin" and \end" suÆxes for the markers. For the ompiler these annotations are regarded as just omments
and hene, will have no bearing on either exeution or
ompilation. In the following blok of Esterel ode,
\blok 1 begin" and \blok 1 end" are two markers.
These two markers an be used to speify the timing
onstraints for the exeution of the ode segment between these two markers.
the timing onstraints to be satised for keeping the logial
properties invariant.
If the ode given is loop-free, then it is oneivable that
validating the onstraints is trivial. However, in the presene of a loop as is the ase in the example, it is not lear as
to how the onstraints an be validated over all the possible omputations. In fat, if the language is treated as just
another imperative language, the answer is not easy as one
has to aount for the various interleaved interations of the
dierent instanes of the body of the loop. However, in the
ontext of Esterel whih is a perfetly synhronous language [?℄ it is neessary to onsider the interations of the
dierent exeution instants of the body due to the global notion of the instant. In the ase of Esterel (or any perfetly
synhronous language):
1. Outputs are produed synhronously with the inputs;
i.e., reations to inputs happen in zero time (an innitely fast mahine). This is in priniple the perfet synhrony hypothesis. At a programming language
level, this is interpreted as: ontrol and Communiations are ompiled away.
%# blok_1_begin
Y := 100;
emit S1(Y);
Y := Y + 100;
X := 7;
emit S2(Y)
%# blok_1_end
Note: (i) The names of the time markers are unique,
and (ii) Markers an be nested but does not inlude
any statement of Esterel that does not terminate in
the same instant.
2.
2. The behaviour an be treated as an innite sequene
of reations (onsisting of inputs and outputs), eah
reation is referred to as an instant. A reation takes
plae on the ourrene of every external event and a
speial signal tik denotes the ourrene of an instant.
1. Introdue additional signals that arry the timing information speied along with the signals of the program without aeting the temporal properties of the
program; emission of additional signals keeps the original timing properties invariant follows from the synhrony hypothesis.
2. Derive the global transition system of the program.
3. From the transitions and the synhrony hypothesis,
derive the global timing onstraints.
Some of the above aspets are further detailed below.
3. VALIDATING TIMING CONSTRAINTS
3.1
Specifying Time Constraints
Timed annotation needs the use of:
1. Time markers: The rst aspet of annotations is
to loate ontrol points through the introdution of
named markers at various points (ontrol) in the soure
program. We use \%# some name"` to denote a marker
at some point of the soure program. For onveniene
the various markers: For instane, we ould have
the following onstraints on the markers blok begin
and blok end:
time(blok end)
time(blok begin) 4 units
In other words, we need to relate the various markers
relative to lok time similar to that given in Table ??.
We use the fragment of speiation language used in
TimeC [?℄ that are needed for synhronous languages.
In fat, sine Esterel interfaes with C-language, we
ould use the omplete language.
3. Inputs are indeterminate; however reation to any input is nite. Hene, the eets are not arried from
one instant to another exept for reording states.
Thus, in the ontext of Esterel validating the timing onstraints orresponds to validating perfet synhroniity. This
an be done by looking at all possible reations from one instant to another. In other words, if the program onsists of
just one module then the illustration shown an be generalized naturally. However, in the ontext of several modules
it beomes nontrivial.
With the given annotated program, the timing onstraints
an be obtained broadly through the following steps:
Language for speifying time onstraints among
3.2
Validating Timing Constraints
The main steps of validating timing onstraints in Esterel programs without loal signals are desribed below:
1. Annotate the Esterel program with markers as disussed above. Compute the stati time relative to
the markers by traversing the ode segment between a
\begin" marker and its orresponding \end" marker.
This is done reursively. Sine, no instant-denable
statement an be there within the marked ode segments (note that in the loop-onstrut of Esterel
there should be at least instant oriented statement to
avoid ausality), the proedure essentially amounts to
traversing a straight line ode in eah module.
2. Add additional signals with orrespondene to Time
markers. That is, for signals of the form
\some name begin" add the statement
emit some name begin zero
at that point where suÆx \zero" indiates that the
time required is zero; for signals of the form
\some name end" add the statement
emit some name end Amount
at that point where suÆx \Amount" is the maximum
time that an elapse from the point of emission of
the signal \some name begin". Note that the value of
\Amount" needs to be a statially evaluatable value.
The omputation of these values is quite easy as no
time-delay operators are allowed as mentioned already.
Note that adding the additional emitting statements
for the logial/ghost signals does not alter either the
funtional or the timing properties of the program due
Esterel source with markers
& time constraints
yes
no
Validation
used in traing the orresponding soure fragments (note
that marker signals keep trak of the ontrol information).
fc2
Preprocessor
oc
Esterel code
Composition &
Computation
time
constraints
fc2
Location & Time
Concatenation
strl
Esterel
Compiler
blif
Xeve
Figure 3: Tool for Validating Time Constraints
to synhrony hypothesis. For onveniene (will be
used in the implementation tool), we ategorize signals
based upon whether they are part of time onstraint
speiation or not as follows:
1. Lsignals: Signals that are neither lok nor time
referenes; in other words, these are signals that are
pure synhronous signals.
2. Tsignals: Those signals that refer to loks are
time onstrained; these inlude the signals introdued
for eah of the markers as in (2) above.
In this presentation, we have assumed that timing information is arried expliitly in the markers.
3. Obtain the reative automaton for the program. Note
that the transitions of the reative automaton arry
the marker-signals introdued.
4. For eah transition ompute the maximum time required. In the pure synhronous approah, all the signals are expeted to our at the same time. However,
in the ontext of time-onstraints, there is a need to
evaluate the time needed for all the miro-steps spread
aross the modules in the same instant; in other words,
one has to arrive at an expression whih would learly
dene the partial order of steps involved (note that
time markers arry the ontrol information).
5. Finally, show that the maximum time for any reation
is less than the minimum time between any two instants (or the tiks) of the reative automaton { thus,
satisfying synhrony hypothesis.
4. IMPLEMENTATION OVERVIEW
The tool is being built using the lassial ode generation tools of the Esterel environment having a struture
as shown in Figure ??. The preproessor omputes the time
requirements relative to the markers speied in the soure
language. In the next blok the dummy statements of emission reeting time requirements for the time-marker signals
are added. The Esterel soure with these additional statements arrying timing information beomes the input to the
strl proessor that generates intermediate ode by ignoring
the omments relative to the timing speiation.
From the f2 ode and o ode generated, the time requirement for eah transition is omputed. The resultant is
the time marked reative automaton in f2 format. In the
validation proess, eah transition is heked for the satisfation of the synhrony hypothesis. The suessful exhaustion of the transitions validates the system relative to the
speiations. Otherwise, it denotes invalidation of the timing onstraints and the underlying tools of Esterel an be
5. DISCUSSIONS
In this paper, we have skethed a method and the design
of a tool for validating the timing onstraints relative to
the speed of the underlying arhiteture, assuring that the
implementation is a realization of the logial synhronous
language speiation. The tool is under implementation
and the generalized tool will validate timing assumptions or
onstraints; it will also provide the sheduling onstraints
on the various asynhronous onstruts that ould be instantiated { for example, through the exe in Esterel .
The tool diagnoses the invalidating transitions with pointers to the respetive ode segments in the Esterel soure.
We also intend to use the tool to validate the timing onstraints and other notions suh as guarantee in real-time
systems as envisaged through Timed CRP - a generalization of Communiating reative proesses [?, ?℄ that unies
the asynhronous and synhronous paradigms.
One of the distint advantages of synhronous framework
is that it establishes the logial orretness of the system.
Sine, the intermediate representation (a kind of automata)
is lose to implementation models, the impliation is that
one has veried the implementation itself. However, sine
the synhronous formalism is based on synhrony hypothesis, it does not onsider the arhitetural onstraints with
referene to time, and asynhronous interfaes. The methodology proposed in the paper provides to bridge suh a gap.
We have been experimenting on the method on various embedded systems using suh a methodology.
For further details the reader is referred to the full paper.
6. REFERENCES
[1℄ Rajeev Alur and David L Dill. A theory of timed
automata. TCS, 126:183{235, 1994.
[2℄ Rajeev Alur and T. Henzinger. Logis and models of
real time: A survey. In REX Workshop on Real-Time:
Theory in Pratie, LNCS, 600, pages 74{106. Springer
Verlag, 1992.
[3℄ G. Berry and A. Benveniste. Synhronous approah to
reative and real-time systems: Another look at
real-time programming. Pro. IEEE, 79:1270{1282,
1991.
[4℄ G Berry, S Ramesh, and R K Shyamasundar.
Communiating Reative Proesses. In 20th POPLS,
pages 85{99, 1993.
[5℄ Gerard Berry and G Gonthier. The ESTEREL
syhronous programming language: Design, semantis,
implementation. SCP, 19(2):87{152, 1992.
[6℄ P. Caspi, D. Pilaud, N. Halbwahs, and J. Plaie.
LUSTRE: A delarative language for programming
synhronous systems. In 14th POPLS, January 1987.
[7℄ Allen Leung, Krishna V Palem, and Amir Pnueli.
TimeC: A time onstraint language for ILP proessor
ompilation. In 5th Australian Conf. on Parallel & Real
Time Systems, pages 57{71. Springer Verlag, 1998.
[8℄ R K Shyamasundar. Programming dynami real-time
systems in rp. In Pro. of the CSA Jubilee Workshop
on Computing and Intelligent Systems, pages 76{89.
Tata-MGraw Hill Publishing Co., 1994.
1/--страниц
Пожаловаться на содержимое документа