[L5] ================================================ AMAST Links 02 03

   Performance-Oriented Specification of Communication Protocols and 
   Verification of Deterministic Bounds of their QoS Characteristics
         PhD-Thesis, Technical University Berlin, Nov. 1994,
                         by Ina Schieferdecker

  The need for performance considerations at each level of the
communication protocol development process arose and were forced by the
advances in high-speed networks and the evolution of new communication
services with their rigorous Quality-of-Service (QoS) requirements.

  This dissertation presents an approach for the QoS-oriented design of
communication protocols using formal specifications. It includes a
specification technique for the performance-oriented behavior
description of communication protocols, a real-time temporal logic for
the description of deterministic bounds, which are a special kind of
QoS requirements, and decision procedures for verifying the
fulfilment of deterministic bounds by a given communication protocol.

  The developed performance-oriented specification technique LotoTis
extends LOTOS --- a standardized specification technique based on
process algebras --- by means of quantified time, quantified
parallelism, quantified nondeterminism, and monitoring of system
execution. The central concept are structured actions which allow very
concise and elegant description of performance-oriented behavior. The
presented approach uses a real-time temporal logic called AMTL, the
action-based version of MTL, for the description of deterministic
bounds of performance characteristics. Deterministic bounds can be
proven to be fulfilled by a given LotoTis protocol specification
provided the specification possesses only a finite --- but possibly
cyclic --- state space. The implementation of the developed
verification method is conceived, which allows us to investigate
realistic communication protocols.

  Author's WWW page at URL: http://www.fokus.gmd.de/htbin/info/step/ina