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. Thesis (Doctoral), Facultad de Informática (UPM).

Description

Title: Síntesis de protocolos de comunicación a partir de especificaciones de servicio
Author/s:
  • Pavón Mestras, Juan
Contributor/s:
  • García Tomás, Jesús
Item Type: Thesis (Doctoral)
Date: 1988
Subjects:
Freetext Keywords: 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
Faculty: Facultad de Informática (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (6MB) | Preview

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.

More information

Item ID: 46778
DC Identifier: http://oa.upm.es/46778/
OAI Identifier: oai:oa.upm.es:46778
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 14 Jun 2017 08:06
Last Modified: 14 Jun 2017 08:06
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM