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.