Abstract
En una arquitectura de interconexión de sistemas, como es el caso del
modelo de referencia de OSI, el requisito principal que debe satisfacer un
protocolo es proporcionar un determinado servicio a las entidades usuarias
del nivel superior. Asimismo, en el diseño del protocolo es necesario considerar
el servicio que ofrece el nivel inferior. Partiendo de este hecho, en
este trabajo se desarrolla un método de síntesis de protocolos pares a partir
de especificaciones de servicios.
Primero se discute el estado de aplicación de las técnicas de descripción
formal en el diseño de protocolos, haciendo un breve repaso a los métodos
de verificación y síntesis de protocolos existentes.
Seguidamente se presenta un lenguaje para la especificación de servicios
(LES) basado en una lógica temporal lineal. Un servicio de nivel se especifica
en LES como un conjunto de fórmulas temporales que definen las relaciones
que pueden existir en la ocurrencia de primitivas de servicio. La aplicación
del lenguaje se ilustra con los servicios proporcionados por los protocolos
tipo de Bit Alternante y Abracadabra.
Utilizando especificaciones de servicios en LES se plantea un método
basado en reglas de transformación que sintetiza dos entidades de
protocolo, expresadas con un lenguaje basado en un modelo de autómatas
finitos comunicantes denominado LEP (Lenguaje de Especificación de Protocolos).
Se muestra la aplicación del método con la síntesis de los protocolos
de Bit Alternante y Abracadabra sobre un medio dúplex con pérdidas. Finalmente se discute el desarrollo de un entorno de diseño de protocolos
basado en los lenguajes LES y LEP, utilizando el método de síntesis
desarrollado y mostrando la relación de LEP con las técnicas de especificación
EstelleySDL.---ABSTRACT---In a computer network architecture, e.g. the OSI Reference Model, the
main requirement to be satisfied by a protocol is the conformance with a
specified service. The protocol has to provide a service to the user entities
which are in the upper layer. Also, the protocol design has to consider the
service provided by the lower layers. It can therefore be seen that the
service concept has a great importance; that is the reason of developing in
this work a synthesis 'method to obtain peer protocols from service
specifications. Its contents is as follows.
Firstly, the state of the art in formal description techniques for protocol
design is shown, reviewing the existing protocol synthesis and verification
methods.
Then, a language for service specification (named LES) based on a linear
temporal logic formalism is presented. A layer service is specified with LES
as a set of temporal formulae. Each of these formulae defines relations
among events (service primitives). The use of the language is shown with
several examples, among them the services provided by the Alternating Bit
and the Abracadabra protocols.
Using service specifications with LES, a method to synthesize two
protocol entities, based on transformation rules, is shown. The protocol
entities are described with LEP, a language based on a communicating finite
state machine model. The method is illustrated by synthesizing two
examples: the Alternating Bit and the Abracadabra protocols, both over a Finally, the development of a protocol design environment is discussed.
This is based on LES and LEP languages, the synthesis method and the
relationship of LEP with Estelle and SDL.
