Information Technology Reference
In-Depth Information
logic over their first order equivalents (such as the real-time logic RTL) allows us to
express a wider range of requirements including liveness properties. QTL is devel-
oped for the specification of distributed multimedia system requirements. QTL is
based upon Koymans' metric temporal logic, MTL, which has already been demon-
strated to be highly suitable for the expression of a wide range of real-time properties
in the area of real-time control. QTL is designed specifically to be compatible with
LOTOS and hence LOTOS events may be used as propositions in QTL. Characteris-
tics of the logic are that it is linear time, it uses bounded operators, it employs a dis-
crete time domain, it uses a basic set of operations (addition by constant only) and it
incorporates past-tense operators as well as the more usual future-tense operators.
QTL has been defined to be suitable for use in conjunction with LOTOS. However,
as well as referring to LOTOS events, there is also a need to refer to data variables in
QTL formulae. These data variables are necessary in order to store additional nu-
merical information such as the number of occurrences of a particular LOTOS event
or, more generally, arbitrary functions over event occurrences and their timings[11].
The functional requirements are given by LOTOS as follows[30]:
specification Multimedia_stream[start, play, error]: noexit
Behavior
start;(hide source_out, sink_in, loss in
((Source[source_out]||| Sink[sink_in, play,error] )
|[source_out,sink_in]|
Channel[source_out,sink_in,loss]))
where
process Source[source_out]:noexit:=
source_out; Source[source_out]
endproc(*Source*)
process Sink[sink_in, play,error]:noexit:=
SinkBehaviour[sink_in,play] [>error;stop
where
process SinkBehaviour[sink_in,play]:noexit:=
sink_in;play;SinkBehaviour[sink_in,play]
endproc(*SinkBehaviour*)
endproc(*Sink*)
process Channel[source_out,sink_in,loss]:noexit:=
Source_out;((sink_in;stop (*frame is transmitted successfully*)
[]loss;stop (*frame is lost during transmission*)
)
|||Channel[source_out,sink_in]) (*allow another frame to be sent*)
endproc(*Channel*)
endspec(*Stream*)
The above functional description is now extended with real-time assumptions. These
constraints are assumed to be described with QTL formulae. Each formula is assumed
to describe a local property for each component of the functional specification[30].
Search WWH ::




Custom Search