Software de Comunicaciones
E.T.S.I. Telecomunicación
Curso 2004/2005
OBJETIVOS:
Esta asignatura está orientada a que el alumno sea capaz de construir prototipos de protocolos y de analizar su corrección empleando entornos de desarrollo basados en ordenador. Se asume que en las asignaturas troncales y obligatorias anteriores el alumno ha estudiado los protocolos en redes de ordenadores desde un punto de vista fundamentalmente descriptivo. Ahora se trata de profundizar en los aspectos de especificación rigurosa y análisis automático de la corrección de los protocolos como paso previo a su implementación, así como en la generación automática de código a partir de las especificaciones correctas de los mismos. Este enfoque es complementario del que se sigue en la asignatura Laboratorio de Software de Comunicaciones.
1. INTRODUCCIÓN A LA INGENIERÍA DE PROTOCOLOS. 1.1. Problemática en el diseño e implementación de protocolos. 1.2. Ciclo de vida en Ingeniería de protocolos. 2. LENGUAJES PARA DESCRIPCIÓN DE PROTOCOLOS. 2.1. Definición y Clasificación de las TDFs(Técnicas de Descripción Formal). 2.2. Máquinas de estados finitos comunicantes (CFSM). 2.3. El lenguaje Promela. 3. VALIDACIÓN AUTOMÁTICA DE PROTOCOLOS. 3.1. Clasificación de los requisitos de corrección. 3.2. Técnicas básicas de validación. 3.3. Métodos de optimización. 3.4. Validación con SPIN. 4. VERIFICACIÓN AUTOMÁTICA DE PROTOCOLOS. 4.1. Lenguajes de especificación de requisitos. 4.1.1. Autómatas de Büchi. 4.1.2. Lógica Temporal. 4.1.3. Diagramas de Secuencia de Mensajes (MSC) 4.2. Especificación y verificación de propiedades con Promela/SPIN. 4.2.1. Asertos. 4.2.2. Never claim. 4.2.3. Lógica temporal en SPIN/XSPIN. 4.3. Recomendaciones de metodología para uso de SPIN(Ejemplo) 5. CASOS PRÁCTICOS (I) 5.1. Especificación, validación y verificación con Promela/SPIN 6. ESPECIFICACIÓN DE PROTOCOLOS CON SDL. 6.1. Estructura de una especificación. 6.2. Definición del comportamiento. 6.3. Datos 6.4. Uso del tiempo. 6.5. Variables compartidas. 6.6. Tendencia del lenguaje, nuevas versiones. 6.7. SDL en la herramienta SDT. 6.8 Otras herramientas para SDL. 7. VALIDACION Y VERIFICACIÓN CON SDL/SDT. 7.1. Validación de SDL con SDT. 7.2. Especificación y verificación de propiedades con SDL/SDT. 7.2.1. Asertos y Reglas de usuario. 7.2.2. MSCs. 7.2.3. Observadores. 8. CASOS PRÁCTICOS (II) 8.1. Especificación, validación y verificación con SDL/SDT. 9. OTRAS FASES EN INGENIERÍA DE PROTOCOLOS (Prácticas demostrativas y/o trabajos voluntarios) 9.1. Análisis de requisitos (uBet) 9.2. Generación de código (Cmicro) 9.3. Análisis de protocolos mediante captura en la red (Analizadores de HP/Agilent).
9.4. Análisis de
prestaciones con ns2
BIBLIOGRAFÍA BÁSICA:
HOLZMANN G. Design and Validation of Computer protocols.
Prentice Hall.1991
HOLZNANN
G. The Model Checker SPIN, 2004
Doldi L.. SDL Illustrated - visually design executable models. Illustrated. 2001.
MATERIAL COMPLEMENTARIO:
BELINA F. Y HOGREFE D. Introduction to SDL 88 - (Tutorial en HTML)
G. HOLZMANN . Documentación y fuentes de la herramienta SPIN.
FARGEMAN O.
Y ANDERS O. New Features in SDL-92 (Tutorial)
TELELOGIC. Documentación de la herramienta SDT.
Enunciado
práctica 1 (SDL básico)
Especificacion SDL Ejemplo Observador
Pedro Merino pedro@lcc.uma.es
Tutorias:
Lunes: 15:30 – 18:30
Jueves: 9 – 12
Despacho: 3.2.9