| Techreport |
| Type of Publication |
| Formal Methods for Broadband and Multimedia
Systems |
| Title |
|
Stefan Leue
|
| Authors |
| Technical Report Dpartment d'IRO, University of Montreal (Quebec),
Canada, 1997 |
| Published in |
| The proper capture of desired system
properties is a pivotal step in providing high quality systems.
The formal specifications of these properties is necessary to
provide unambiguous documentation as well as automated
transformation of system requirements during all stages of the
life cycle. The standardized Formal Description Techniques (FDTs)
Estelle and SDL have proved useful for the specification of
traditional protocols and distributed systems. With the
availability of high-speed networks new applications with
additional requirements and characteristics are becoming reality.
These requirements are often referred to as Quality of Service
(QoS) requirements.We show that the above mentioned FDTs do not
possess the expressiveness to capture importaqnt classes of QoS
requirements, namely quantitative deterministic real-time-related
properties. It is the purpose of this paper to exemplify steps
that need to be taken in order to overcome this deficit. We first
discuss choices that need to be made when designing a suitable
real-time execution model SDL and Estelle and proceed to present
two remedies to the inexpressiveness problem: First, we introduce
the concept of complementary real-time specification by
reconciling the semantic models of Metric Temporal Logic and SDL
and showing how both languages can be used in a complementary
fashion. Second, we suggest a language extension and the
corresponding semantic interpretation for Estelle. While we
present examples from the domain of multimedia and broadband
systems, the applicability of our specification methodes extends
to hard real-time systems. Finally, we discuss extensions of our
techniques to capture QoS stochastic properties, and we allude to
formal requirements verification and automatic implementation
based on our techniques. |
| Abstract |
| [PDF]
[BIB] [XML] |
| Downloads & Bib-Entries |
