Towards the automatic generation of quality-of-service-preserving implementations from formal specifications

The possibility to automatically generate implementations from formal specifications of distributed systems and protocols is one of the major advantages of the use of formal methods. This process is well understood for standardized Formal Description Techniques (FDTs) such as Estelle, SDL and LOTOS applied to traditional communication protocols. In order to use these languages for the specification of modern telecommunication systems such as multimedia, which is addition, have certain real-time requirements, several real-time language enhancements have been proposed. In this article, we show how, based on a real-time extension of Estelle, implementations can be generated that are able to automatically guarantee specified real-time requirements during the system's runtime.