Síntesis de protocolos de comunicación a partir de especificaciones de servicio

Pavón Mestras, Juan (1988). Síntesis de protocolos de comunicación a partir de especificaciones de servicio. Tesis (Doctoral), Facultad de Informática (UPM) [antigua denominación].

Descripción

Título: Síntesis de protocolos de comunicación a partir de especificaciones de servicio
Autor/es:
  • Pavón Mestras, Juan
Director/es:
  • García Tomás, Jesús
Tipo de Documento: Tesis (Doctoral)
Fecha: 1988
Materias:
Palabras Clave Informales: Autómatas Finitos Comunicantes; Especificación formal; Estelle; Ingeniería de Protocolos; Lógica Temporal; OSI; Protocolo; Reglas de Transformación; SDL; Servicio; Síntesis de Protocolos; Técnica de Descripción Formal; Verificación de Protocolos; Communicating Finite State Machines; Formal Description Technique; Formal Specification; Protocol Engineering; Protocol Synthesis; Protocol Verification; Service; Temporal Logic; Transformation Rules
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (6MB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 46778
Identificador DC: http://oa.upm.es/46778/
Identificador OAI: oai:oa.upm.es:46778
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 14 Jun 2017 08:06
Ultima Modificación: 14 Jun 2017 08:06
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM